Theorem cbvrex 1790

Description: Rule used to change bound variables with implicit substitution.

Hypotheses

Ref	Expression
cbvral.1	⊢ (φ → ∀yφ)
cbvral.2	⊢ (ψ → ∀xψ)
cbvral.3	⊢ (x = y → (φ ↔ ψ))

Assertion

Ref	Expression
cbvrex	⊢ (∃x ∈ A φ ↔ ∃y ∈ A ψ)

Distinct variable group:   x,y,A

Proof of Theorem cbvrex

Step	Hyp	Ref	Expression
1		ax-17 968	. . . 4 ⊢ (x ∈ A → ∀y x ∈ A)
2		cbvral.1	. . . 4 ⊢ (φ → ∀yφ)
3	1, 2	hban 1006	. . 3 ⊢ ((x ∈ A ⋀ φ) → ∀y(x ∈ A ⋀ φ))
4		ax-17 968	. . . 4 ⊢ (y ∈ A → ∀x y ∈ A)
5		cbvral.2	. . . 4 ⊢ (ψ → ∀xψ)
6	4, 5	hban 1006	. . 3 ⊢ ((y ∈ A ⋀ ψ) → ∀x(y ∈ A ⋀ ψ))
7		eleq1 1526	. . . 4 ⊢ (x = y → (x ∈ A ↔ y ∈ A))
8		cbvral.3	. . . 4 ⊢ (x = y → (φ ↔ ψ))
9	7, 8	anbi12d 626	. . 3 ⊢ (x = y → ((x ∈ A ⋀ φ) ↔ (y ∈ A ⋀ ψ)))
10	3, 6, 9	cbvex 1162	. 2 ⊢ (∃x(x ∈ A ⋀ φ) ↔ ∃y(y ∈ A ⋀ ψ))
11		df-rex 1642	. 2 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))
12		df-rex 1642	. 2 ⊢ (∃y ∈ A ψ ↔ ∃y(y ∈ A ⋀ ψ))
13	10, 11, 12	3bitr4 183	1 ⊢ (∃x ∈ A φ ↔ ∃y ∈ A ψ)

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  ∃wex 977  ∃wrex 1638

This theorem is referenced by:  cbvrexv 1792  cbvrexsv 1958  cbviun 2579  isarep1 3563  elrnopabg 3785  abrexexlem2 3844  elrnoprabg 4108  cau3i 6851

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465  df-rex 1642

Copyright terms: Public domain