Mathbox for Alan Sare < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  2uasbanhVD Structured version   Visualization version   GIF version

Theorem 2uasbanhVD 41632
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 41290) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 41282 is 2uasbanhVD 41632 without virtual deductions and was automatically derived from 2uasbanhVD 41632. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
 h1:: ⊢ (𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) 100:1: ⊢ (𝜒 → (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) 2:100: ⊢ (   𝜒   ▶   (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))   ) 3:2: ⊢ (   𝜒   ▶   ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ) 4:3: ⊢ (   𝜒   ▶   ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )   ) 5:4: ⊢ (   𝜒   ▶   (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)    ) 6:5: ⊢ (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))   ) 7:3,6: ⊢ (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   ) 8:2: ⊢ (   𝜒   ▶   ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)   ) 9:5: ⊢ (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))   ) 10:8,9: ⊢ (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜓   ) 101:: ⊢ ([𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓)) 102:101: ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓)) 103:: ⊢ ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦 ]𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) 104:102,103: ⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) 11:7,10,104: ⊢ (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓)   ) 110:5: ⊢ (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)))   ) 12:11,110: ⊢ (   𝜒   ▶   ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))   ) 120:12: ⊢ (𝜒 → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ (𝜑 ∧ 𝜓))) 13:1,120: ⊢ ((∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))) 14:: ⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))   ) 15:14: ⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   ) 16:14: ⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   (𝜑 ∧ 𝜓)   ) 17:16: ⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   𝜑   ) 18:15,17: ⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   ) 19:18: ⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) 20:19: ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) 21:20: ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) 22:16: ⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   𝜓   ) 23:15,22: ⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)   ) 24:23: ⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) 25:24: ⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) 26:25: ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) 27:21,26: ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦( (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))) qed:13,27: ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦( (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))
Hypothesis
Ref Expression
2uasbanhVD.1 (𝜒 ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
Assertion
Ref Expression
2uasbanhVD (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣   𝑦,𝑣
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑣,𝑢)   𝜓(𝑥,𝑦,𝑣,𝑢)   𝜒(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem 2uasbanhVD
StepHypRef Expression
1 idn1 41295 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   )
2 simpl 486 . . . . . . . 8 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → (𝑥 = 𝑢𝑦 = 𝑣))
31, 2e1a 41348 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   (𝑥 = 𝑢𝑦 = 𝑣)   )
4 simpr 488 . . . . . . . . 9 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → (𝜑𝜓))
51, 4e1a 41348 . . . . . . . 8 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   (𝜑𝜓)   )
6 simpl 486 . . . . . . . 8 ((𝜑𝜓) → 𝜑)
75, 6e1a 41348 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   𝜑   )
8 pm3.2 473 . . . . . . 7 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝜑 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
93, 7, 8e11 41409 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
109in1 41292 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
1110eximi 1836 . . . 4 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
1211eximi 1836 . . 3 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
13 simpr 488 . . . . . . . 8 ((𝜑𝜓) → 𝜓)
145, 13e1a 41348 . . . . . . 7 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   𝜓   )
15 pm3.2 473 . . . . . . 7 ((𝑥 = 𝑢𝑦 = 𝑣) → (𝜓 → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
163, 14, 15e11 41409 . . . . . 6 (   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   ▶   ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)   )
1716in1 41292 . . . . 5 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
1817eximi 1836 . . . 4 (∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
1918eximi 1836 . . 3 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
2012, 19jca 515 . 2 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
21 2uasbanhVD.1 . . 3 (𝜒 ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
2221biimpi 219 . . . . . . . . 9 (𝜒 → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
2322dfvd1ir 41294 . . . . . . . 8 (   𝜒   ▶   (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))   )
24 simpl 486 . . . . . . . 8 ((∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))
2523, 24e1a 41348 . . . . . . 7 (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)   )
26 simpl 486 . . . . . . . . . . 11 (((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → (𝑥 = 𝑢𝑦 = 𝑣))
27262eximi 1837 . . . . . . . . . 10 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
2825, 27e1a 41348 . . . . . . . . 9 (   𝜒   ▶   𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)   )
29 ax6e2ndeq 41280 . . . . . . . . . 10 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) ↔ ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3029biimpri 231 . . . . . . . . 9 (∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣) → (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣))
3128, 30e1a 41348 . . . . . . . 8 (   𝜒   ▶   (¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣)   )
32 2sb5nd 41281 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)))
3331, 32e1a 41348 . . . . . . 7 (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑))   )
34 biimpr 223 . . . . . . . 8 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)) → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3534com12 32 . . . . . . 7 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑)) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
3625, 33, 35e11 41409 . . . . . 6 (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
37 simpr 488 . . . . . . . 8 ((∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))
3823, 37e1a 41348 . . . . . . 7 (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)   )
39 2sb5nd 41281 . . . . . . . 8 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
4031, 39e1a 41348 . . . . . . 7 (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓))   )
41 biimpr 223 . . . . . . . 8 (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
4241com12 32 . . . . . . 7 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓) → (([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
4338, 40, 42e11 41409 . . . . . 6 (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜓   )
44 sban 2085 . . . . . . . 8 ([𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
4544sbbii 2081 . . . . . . 7 ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
46 sban 2085 . . . . . . 7 ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
4745, 46bitri 278 . . . . . 6 ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
48 simplbi2comt 505 . . . . . . 7 (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓))))
4948com13 88 . . . . . 6 ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 → (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓)) → [𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓))))
5036, 43, 47, 49e110 41397 . . . . 5 (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓)   )
51 2sb5nd 41281 . . . . . 6 ((¬ ∀𝑥 𝑥 = 𝑦𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))))
5231, 51e1a 41348 . . . . 5 (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)))   )
53 biimp 218 . . . . . 6 (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))) → ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))))
5453com12 32 . . . . 5 ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) → (([𝑢 / 𝑥][𝑣 / 𝑦](𝜑𝜓) ↔ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))))
5550, 52, 54e11 41409 . . . 4 (   𝜒   ▶   𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓))   )
5655in1 41292 . . 3 (𝜒 → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)))
5721, 56sylbir 238 . 2 ((∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)))
5820, 57impbii 212 1 (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ (𝜑𝜓)) ↔ (∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥𝑦((𝑥 = 𝑢𝑦 = 𝑣) ∧ 𝜓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∀wal 1536   = wceq 1538  ∃wex 1781  [wsb 2069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-v 3443  df-vd1 41291 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator