Theorem cbvrexf 10338

Description: Rule used to change bound variables with implicit substitution. More general than cbvrex 1790.

Hypotheses

Ref	Expression
cbvrexf.1	⊢ (z ∈ A → ∀x z ∈ A)
cbvrexf.2	⊢ (z ∈ A → ∀y z ∈ A)
cbvrexf.3	⊢ (φ → ∀yφ)
cbvrexf.4	⊢ (ψ → ∀xψ)
cbvrexf.5	⊢ (x = y → (φ ↔ ψ))

Assertion

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

Distinct variable groups:   z,A   x,y,z

Proof of Theorem cbvrexf

Step	Hyp	Ref	Expression
1		ax-17 968	. . . . 5 ⊢ (z ∈ x → ∀y z ∈ x)
2		cbvrexf.2	. . . . 5 ⊢ (z ∈ A → ∀y z ∈ A)
3	1, 2	hbel 1558	. . . 4 ⊢ (x ∈ A → ∀y x ∈ A)
4		cbvrexf.3	. . . 4 ⊢ (φ → ∀yφ)
5	3, 4	hban 1006	. . 3 ⊢ ((x ∈ A ⋀ φ) → ∀y(x ∈ A ⋀ φ))
6		ax-17 968	. . . . 5 ⊢ (z ∈ y → ∀x z ∈ y)
7		cbvrexf.1	. . . . 5 ⊢ (z ∈ A → ∀x z ∈ A)
8	6, 7	hbel 1558	. . . 4 ⊢ (y ∈ A → ∀x y ∈ A)
9		cbvrexf.4	. . . 4 ⊢ (ψ → ∀xψ)
10	8, 9	hban 1006	. . 3 ⊢ ((y ∈ A ⋀ ψ) → ∀x(y ∈ A ⋀ ψ))
11		eleq1 1526	. . . 4 ⊢ (x = y → (x ∈ A ↔ y ∈ A))
12		cbvrexf.5	. . . 4 ⊢ (x = y → (φ ↔ ψ))
13	11, 12	anbi12d 626	. . 3 ⊢ (x = y → ((x ∈ A ⋀ φ) ↔ (y ∈ A ⋀ ψ)))
14	5, 10, 13	cbvex 1162	. 2 ⊢ (∃x(x ∈ A ⋀ φ) ↔ ∃y(y ∈ A ⋀ ψ))
15		df-rex 1642	. 2 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ⋀ φ))
16		df-rex 1642	. 2 ⊢ (∃y ∈ A ψ ↔ ∃y(y ∈ A ⋀ ψ))
17	14, 15, 16	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 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