ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  copsex2t GIF version

Theorem copsex2t 4266
Description: Closed theorem form of copsex2g 4267. (Contributed by NM, 17-Feb-2013.)
Assertion
Ref Expression
copsex2t ((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) ∧ (𝐴𝑉𝐵𝑊)) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Distinct variable groups:   𝑥,𝑦,𝜓   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑉(𝑥,𝑦)   𝑊(𝑥,𝑦)

Proof of Theorem copsex2t
StepHypRef Expression
1 elisset 2766 . . . 4 (𝐴𝑉 → ∃𝑥 𝑥 = 𝐴)
2 elisset 2766 . . . 4 (𝐵𝑊 → ∃𝑦 𝑦 = 𝐵)
31, 2anim12i 338 . . 3 ((𝐴𝑉𝐵𝑊) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
4 eeanv 1944 . . 3 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
53, 4sylibr 134 . 2 ((𝐴𝑉𝐵𝑊) → ∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵))
6 nfa1 1552 . . . 4 𝑥𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
7 nfe1 1507 . . . . 5 𝑥𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
8 nfv 1539 . . . . 5 𝑥𝜓
97, 8nfbi 1600 . . . 4 𝑥(∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)
10 nfa2 1590 . . . . 5 𝑦𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
11 nfe1 1507 . . . . . . 7 𝑦𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211nfex 1648 . . . . . 6 𝑦𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
13 nfv 1539 . . . . . 6 𝑦𝜓
1412, 13nfbi 1600 . . . . 5 𝑦(∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)
15 opeq12 3798 . . . . . . . . 9 ((𝑥 = 𝐴𝑦 = 𝐵) → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
16 copsexg 4265 . . . . . . . . . 10 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
1716eqcoms 2192 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝐵⟩ → (𝜑 ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
1815, 17syl 14 . . . . . . . 8 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑 ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
1918adantl 277 . . . . . . 7 ((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → (𝜑 ↔ ∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
20 sp 1522 . . . . . . . . 9 (∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) → ∀𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)))
212019.21bi 1569 . . . . . . . 8 (∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) → ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)))
2221imp 124 . . . . . . 7 ((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → (𝜑𝜓))
2319, 22bitr3d 190 . . . . . 6 ((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) ∧ (𝑥 = 𝐴𝑦 = 𝐵)) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
2423ex 115 . . . . 5 (∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) → ((𝑥 = 𝐴𝑦 = 𝐵) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)))
2510, 14, 24exlimd 1608 . . . 4 (∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) → (∃𝑦(𝑥 = 𝐴𝑦 = 𝐵) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)))
266, 9, 25exlimd 1608 . . 3 (∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) → (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓)))
2726imp 124 . 2 ((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) ∧ ∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵)) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
285, 27sylan2 286 1 ((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) ∧ (𝐴𝑉𝐵𝑊)) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wal 1362   = wceq 1364  wex 1503  wcel 2160  cop 3613
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4139  ax-pow 4195  ax-pr 4230
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3595  df-sn 3616  df-pr 3617  df-op 3619
This theorem is referenced by:  opelopabt  4283
  Copyright terms: Public domain W3C validator