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

Metamath Proof Explorer

Theorem vtocl2gafOLD

Description: Obsolete version of vtocl2gaf as of 31-May-2025. (Contributed by NM, 10-Aug-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses vtocl2gaf.a ⊢ Ⅎ 𝑥 𝐴
vtocl2gaf.b ⊢ Ⅎ 𝑦 𝐴
vtocl2gaf.c ⊢ Ⅎ 𝑦 𝐵
vtocl2gaf.1 ⊢ Ⅎ 𝑥 𝜓
vtocl2gaf.2 ⊢ Ⅎ 𝑦 𝜒
vtocl2gaf.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
vtocl2gaf.4 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
vtocl2gaf.5 ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 )
Assertion vtocl2gafOLD ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 vtocl2gaf.a ⊢ Ⅎ 𝑥 𝐴
2 vtocl2gaf.b ⊢ Ⅎ 𝑦 𝐴
3 vtocl2gaf.c ⊢ Ⅎ 𝑦 𝐵
4 vtocl2gaf.1 ⊢ Ⅎ 𝑥 𝜓
5 vtocl2gaf.2 ⊢ Ⅎ 𝑦 𝜒
6 vtocl2gaf.3 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
7 vtocl2gaf.4 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
8 vtocl2gaf.5 ⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 )
9 1 nfel1 ⊢ Ⅎ 𝑥 𝐴 ∈ 𝐶
10 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐷
11 9 10 nfan ⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 )
12 11 4 nfim ⊢ Ⅎ 𝑥 ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜓 )
13 2 nfel1 ⊢ Ⅎ 𝑦 𝐴 ∈ 𝐶
14 3 nfel1 ⊢ Ⅎ 𝑦 𝐵 ∈ 𝐷
15 13 14 nfan ⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 )
16 15 5 nfim ⊢ Ⅎ 𝑦 ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )
17 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶 ) )
18 17 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ) )
19 18 6 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜑 ) ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜓 ) ) )
20 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷 ) )
21 20 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) ) )
22 21 7 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷 ) → 𝜓 ) ↔ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 ) ) )
23 1 2 3 12 16 19 22 8 vtocl2gf ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 ) )
24 23 pm2.43i ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝜒 )