NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mob GIF version

Theorem mob 3018
Description: Equality implied by "at most one." (Contributed by NM, 18-Feb-2006.)
Hypotheses
Ref Expression
moi.1 (x = A → (φψ))
moi.2 (x = B → (φχ))
Assertion
Ref Expression
mob (((A C B D) ∃*xφ ψ) → (A = Bχ))
Distinct variable groups:   x,A   x,B   χ,x   ψ,x
Allowed substitution hints:   φ(x)   C(x)   D(x)

Proof of Theorem mob
StepHypRef Expression
1 elex 2867 . . . . 5 (B DB V)
2 nfcv 2489 . . . . . . . 8 xA
3 nfv 1619 . . . . . . . . . 10 x B V
4 nfmo1 2215 . . . . . . . . . 10 x∃*xφ
5 nfv 1619 . . . . . . . . . 10 xψ
63, 4, 5nf3an 1827 . . . . . . . . 9 x(B V ∃*xφ ψ)
7 nfv 1619 . . . . . . . . 9 x(A = Bχ)
86, 7nfim 1813 . . . . . . . 8 x((B V ∃*xφ ψ) → (A = Bχ))
9 moi.1 . . . . . . . . . 10 (x = A → (φψ))
1093anbi3d 1258 . . . . . . . . 9 (x = A → ((B V ∃*xφ φ) ↔ (B V ∃*xφ ψ)))
11 eqeq1 2359 . . . . . . . . . 10 (x = A → (x = BA = B))
1211bibi1d 310 . . . . . . . . 9 (x = A → ((x = Bχ) ↔ (A = Bχ)))
1310, 12imbi12d 311 . . . . . . . 8 (x = A → (((B V ∃*xφ φ) → (x = Bχ)) ↔ ((B V ∃*xφ ψ) → (A = Bχ))))
14 moi.2 . . . . . . . . 9 (x = B → (φχ))
1514mob2 3016 . . . . . . . 8 ((B V ∃*xφ φ) → (x = Bχ))
162, 8, 13, 15vtoclgf 2913 . . . . . . 7 (A C → ((B V ∃*xφ ψ) → (A = Bχ)))
1716com12 27 . . . . . 6 ((B V ∃*xφ ψ) → (A C → (A = Bχ)))
18173expib 1154 . . . . 5 (B V → ((∃*xφ ψ) → (A C → (A = Bχ))))
191, 18syl 15 . . . 4 (B D → ((∃*xφ ψ) → (A C → (A = Bχ))))
2019com3r 73 . . 3 (A C → (B D → ((∃*xφ ψ) → (A = Bχ))))
2120imp 418 . 2 ((A C B D) → ((∃*xφ ψ) → (A = Bχ)))
22213impib 1149 1 (((A C B D) ∃*xφ ψ) → (A = Bχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 176   wa 358   w3a 934   = wceq 1642   wcel 1710  ∃*wmo 2205  Vcvv 2859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861
This theorem is referenced by:  moi  3019  rmob  3134
  Copyright terms: Public domain W3C validator