This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gencbvex

Description: Change of bound variable using implicit substitution. (Contributed by NM, 17-May-1996) (Proof shortened by Andrew Salmon, 8-Jun-2011)

Ref Expression
Hypotheses gencbvex.1 ⊢ 𝐴 ∈ V
gencbvex.2 ⊢ ( 𝐴 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
gencbvex.3 ⊢ ( 𝐴 = 𝑦 → ( 𝜒 ↔ 𝜃 ) )
gencbvex.4 ⊢ ( 𝜃 ↔ ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) )
Assertion gencbvex ( ∃ 𝑥 ( 𝜒 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝜃 ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 gencbvex.1 ⊢ 𝐴 ∈ V
2 gencbvex.2 ⊢ ( 𝐴 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3 gencbvex.3 ⊢ ( 𝐴 = 𝑦 → ( 𝜒 ↔ 𝜃 ) )
4 gencbvex.4 ⊢ ( 𝜃 ↔ ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) )
5 excom ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) )
6 3 2 anbi12d ⊢ ( 𝐴 = 𝑦 → ( ( 𝜒 ∧ 𝜑 ) ↔ ( 𝜃 ∧ 𝜓 ) ) )
7 6 bicomd ⊢ ( 𝐴 = 𝑦 → ( ( 𝜃 ∧ 𝜓 ) ↔ ( 𝜒 ∧ 𝜑 ) ) )
8 7 eqcoms ⊢ ( 𝑦 = 𝐴 → ( ( 𝜃 ∧ 𝜓 ) ↔ ( 𝜒 ∧ 𝜑 ) ) )
9 1 8 ceqsexv ⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ( 𝜒 ∧ 𝜑 ) )
10 9 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ( 𝜒 ∧ 𝜑 ) )
11 19.41v ⊢ ( ∃ 𝑥 ( 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) )
12 simpr ⊢ ( ( ∃ 𝑥 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) → ( 𝜃 ∧ 𝜓 ) )
13 eqcom ⊢ ( 𝐴 = 𝑦 ↔ 𝑦 = 𝐴 )
14 13 biimpi ⊢ ( 𝐴 = 𝑦 → 𝑦 = 𝐴 )
15 14 adantl ⊢ ( ( 𝜒 ∧ 𝐴 = 𝑦 ) → 𝑦 = 𝐴 )
16 15 eximi ⊢ ( ∃ 𝑥 ( 𝜒 ∧ 𝐴 = 𝑦 ) → ∃ 𝑥 𝑦 = 𝐴 )
17 4 16 sylbi ⊢ ( 𝜃 → ∃ 𝑥 𝑦 = 𝐴 )
18 17 adantr ⊢ ( ( 𝜃 ∧ 𝜓 ) → ∃ 𝑥 𝑦 = 𝐴 )
19 18 ancri ⊢ ( ( 𝜃 ∧ 𝜓 ) → ( ∃ 𝑥 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) )
20 12 19 impbii ⊢ ( ( ∃ 𝑥 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ( 𝜃 ∧ 𝜓 ) )
21 11 20 bitri ⊢ ( ∃ 𝑥 ( 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ( 𝜃 ∧ 𝜓 ) )
22 21 exbii ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑦 = 𝐴 ∧ ( 𝜃 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝜃 ∧ 𝜓 ) )
23 5 10 22 3bitr3i ⊢ ( ∃ 𝑥 ( 𝜒 ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝜃 ∧ 𝜓 ) )