2uasbanhVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh is 2uasbanhVD without virtual deductions and was automatically derived from 2uasbanhVD . (Contributed by Alan Sare, 31-May-2014) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	2uasbanhVD.1	⊢ ( 𝜒 ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
	Assertion	2uasbanhVD	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		2uasbanhVD.1	⊢ ( 𝜒 ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
2		idn1	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ▶ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
3		simpl	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
4	2 3	e1a	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ▶ ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
5		simpr	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 ∧ 𝜓 ) )
6	2 5	e1a	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ▶ ( 𝜑 ∧ 𝜓 ) )
7		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
8	6 7	e1a	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ▶ 𝜑 )
9		pm3.2	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝜑 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
10	4 8 9	e11	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ▶ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
11	10	in1	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
12	11	eximi	⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
13	12	eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
14		simpr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 )
15	6 14	e1a	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ▶ 𝜓 )
16		pm3.2	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝜓 → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
17	4 15 16	e11	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ▶ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
18	17	in1	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
19	18	eximi	⊢ ( ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
20	19	eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
21	13 20	jca	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
22	1	biimpi	⊢ ( 𝜒 → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
23	22	dfvd1ir	⊢ ( 𝜒 ▶ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
24		simpl	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
25	23 24	e1a	⊢ ( 𝜒 ▶ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) )
26		simpl	⊢ ( ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
27	26	2eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
28	25 27	e1a	⊢ ( 𝜒 ▶ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
29		ax6e2ndeq	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) )
30	29	biimpri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
31	28 30	e1a	⊢ ( 𝜒 ▶ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) )
32		2sb5nd	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
33	31 32	e1a	⊢ ( 𝜒 ▶ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )
34		biimpr	⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
35	34	com12	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) → ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ) )
36	25 33 35	e11	⊢ ( 𝜒 ▶ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
37		simpr	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
38	23 37	e1a	⊢ ( 𝜒 ▶ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) )
39		2sb5nd	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
40	31 39	e1a	⊢ ( 𝜒 ▶ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )
41		biimpr	⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) )
42	41	com12	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) → ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) )
43	38 40 42	e11	⊢ ( 𝜒 ▶ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 )
44		sban	⊢ ( [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑣 / 𝑦 ] 𝜓 ) )
45	44	sbbii	⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ [ 𝑢 / 𝑥 ] ( [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑣 / 𝑦 ] 𝜓 ) )
46		sban	⊢ ( [ 𝑢 / 𝑥 ] ( [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑣 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) )
47	45 46	bitri	⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) )
48		simplbi2comt	⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ) ) )
49	48	com13	⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 → ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ∧ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ) ) → [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ) ) )
50	36 43 47 49	e110	⊢ ( 𝜒 ▶ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) )
51		2sb5nd	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) )
52	31 51	e1a	⊢ ( 𝜒 ▶ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) )
53		biimp	⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) )
54	53	com12	⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) → ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] ( 𝜑 ∧ 𝜓 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ) )
55	50 52 54	e11	⊢ ( 𝜒 ▶ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
56	55	in1	⊢ ( 𝜒 → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
57	1 56	sylbir	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) → ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) )
58	21 57	impbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ∧ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜓 ) ) )

h1::	\|- ( ch <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
100:1:	\|- ( ch -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
2:100:	\|- (. ch ->. ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
3:2:	\|- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ph ) ).
4:3:	\|- (. ch ->. E. x E. y ( x = u /\ y = v ) ).
5:4:	\|- (. ch ->. ( -. A. x x = y \/ u = v ) ).
6:5:	\|- (. ch ->. ( [ u / x ] [ v / y ] ph <-> E. x E. y ( ( x = u /\ y = v ) /\ ph ) ) ).
7:3,6:	\|- (. ch ->. [ u / x ] [ v / y ] ph ).
8:2:	\|- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ps ) ).
9:5:	\|- (. ch ->. ( [ u / x ] [ v / y ] ps <-> E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) ).
10:8,9:	\|- (. ch ->. [ u / x ] [ v / y ] ps ).
101::	\|- ( [ v / y ] ( ph /\ ps ) <-> ( [ v / y ] ph /\ [ v / y ] ps ) )
102:101:	\|- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) )
103::	\|- ( [ u / x ] ( [ v / y ] ph /\ [ v / y ] ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
104:102,103:	\|- ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> ( [ u / x ] [ v / y ] ph /\ [ u / x ] [ v / y ] ps ) )
11:7,10,104:	\|- (. ch ->. [ u / x ] [ v / y ] ( ph /\ ps ) ).
110:5:	\|- (. ch ->. ( [ u / x ] [ v / y ] ( ph /\ ps ) <-> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ) ).
12:11,110:	\|- (. ch ->. E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
120:12:	\|- ( ch -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
13:1,120:	\|- ( ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) )
14::	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ).
15:14:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( x = u /\ y = v ) ).
16:14:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ph /\ ps ) ).
17:16:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ph ).
18:15,17:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ph ) ).
19:18:	\|- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ph ) )
20:19:	\|- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ph ) )
21:20:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ph ) )
22:16:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ps ).
23:15,22:	\|- (. ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) ->. ( ( x = u /\ y = v ) /\ ps ) ).
24:23:	\|- ( ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( ( x = u /\ y = v ) /\ ps ) )
25:24:	\|- ( E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. y ( ( x = u /\ y = v ) /\ ps ) )
26:25:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> E. x E. y ( ( x = u /\ y = v ) /\ ps ) )
27:21,26:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) -> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )
qed:13,27:	\|- ( E. x E. y ( ( x = u /\ y = v ) /\ ( ph /\ ps ) ) <-> ( E. x E. y ( ( x = u /\ y = v ) /\ ph ) /\ E. x E. y ( ( x = u /\ y = v ) /\ ps ) ) )

Metamath Proof Explorer

Theorem 2uasbanhVD

Proof