MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vtoclgftOLD Structured version   Visualization version   GIF version

Theorem vtoclgftOLD 3241
Description: Obsolete proof of vtoclgft 3240 as of 11-Aug-2021. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 12-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
vtoclgftOLD (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴𝑉) → 𝜓)

Proof of Theorem vtoclgftOLD
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elex 3198 . 2 (𝐴𝑉𝐴 ∈ V)
2 elisset 3201 . . . . 5 (𝐴 ∈ V → ∃𝑧 𝑧 = 𝐴)
323ad2ant3 1082 . . . 4 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → ∃𝑧 𝑧 = 𝐴)
4 nfnfc1 2764 . . . . . . 7 𝑥𝑥𝐴
5 nfcvd 2762 . . . . . . . 8 (𝑥𝐴𝑥𝑧)
6 id 22 . . . . . . . 8 (𝑥𝐴𝑥𝐴)
75, 6nfeqd 2768 . . . . . . 7 (𝑥𝐴 → Ⅎ𝑥 𝑧 = 𝐴)
8 eqeq1 2625 . . . . . . . 8 (𝑧 = 𝑥 → (𝑧 = 𝐴𝑥 = 𝐴))
98a1i 11 . . . . . . 7 (𝑥𝐴 → (𝑧 = 𝑥 → (𝑧 = 𝐴𝑥 = 𝐴)))
104, 7, 9cbvexd 2277 . . . . . 6 (𝑥𝐴 → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴))
1110ad2antrr 761 . . . . 5 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑)) → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴))
12113adant3 1079 . . . 4 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → (∃𝑧 𝑧 = 𝐴 ↔ ∃𝑥 𝑥 = 𝐴))
133, 12mpbid 222 . . 3 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → ∃𝑥 𝑥 = 𝐴)
14 biimp 205 . . . . . . . . 9 ((𝜑𝜓) → (𝜑𝜓))
1514imim2i 16 . . . . . . . 8 ((𝑥 = 𝐴 → (𝜑𝜓)) → (𝑥 = 𝐴 → (𝜑𝜓)))
1615com23 86 . . . . . . 7 ((𝑥 = 𝐴 → (𝜑𝜓)) → (𝜑 → (𝑥 = 𝐴𝜓)))
1716imp 445 . . . . . 6 (((𝑥 = 𝐴 → (𝜑𝜓)) ∧ 𝜑) → (𝑥 = 𝐴𝜓))
1817alanimi 1741 . . . . 5 ((∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) → ∀𝑥(𝑥 = 𝐴𝜓))
19183ad2ant2 1081 . . . 4 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → ∀𝑥(𝑥 = 𝐴𝜓))
20 simp1r 1084 . . . . 5 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → Ⅎ𝑥𝜓)
21 19.23t 2077 . . . . 5 (Ⅎ𝑥𝜓 → (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓)))
2220, 21syl 17 . . . 4 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → (∀𝑥(𝑥 = 𝐴𝜓) ↔ (∃𝑥 𝑥 = 𝐴𝜓)))
2319, 22mpbid 222 . . 3 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → (∃𝑥 𝑥 = 𝐴𝜓))
2413, 23mpd 15 . 2 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴 ∈ V) → 𝜓)
251, 24syl3an3 1358 1 (((𝑥𝐴 ∧ Ⅎ𝑥𝜓) ∧ (∀𝑥(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝜑) ∧ 𝐴𝑉) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036  wal 1478   = wceq 1480  wex 1701  wnf 1705  wcel 1987  wnfc 2748  Vcvv 3186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator