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

Theorem cgsex2g 2891
 Description: Implicit substitution inference for general classes. (Contributed by NM, 26-Jul-1995.)
Hypotheses
Ref Expression
cgsex2g.1 ((x = A y = B) → χ)
cgsex2g.2 (χ → (φψ))
Assertion
Ref Expression
cgsex2g ((A V B W) → (xy(χ φ) ↔ ψ))
Distinct variable groups:   x,y,ψ   x,A,y   x,B,y
Allowed substitution hints:   φ(x,y)   χ(x,y)   V(x,y)   W(x,y)

Proof of Theorem cgsex2g
StepHypRef Expression
1 cgsex2g.2 . . . 4 (χ → (φψ))
21biimpa 470 . . 3 ((χ φ) → ψ)
32exlimivv 1635 . 2 (xy(χ φ) → ψ)
4 elisset 2869 . . . . . 6 (A Vx x = A)
5 elisset 2869 . . . . . 6 (B Wy y = B)
64, 5anim12i 549 . . . . 5 ((A V B W) → (x x = A y y = B))
7 eeanv 1913 . . . . 5 (xy(x = A y = B) ↔ (x x = A y y = B))
86, 7sylibr 203 . . . 4 ((A V B W) → xy(x = A y = B))
9 cgsex2g.1 . . . . 5 ((x = A y = B) → χ)
1092eximi 1577 . . . 4 (xy(x = A y = B) → xyχ)
118, 10syl 15 . . 3 ((A V B W) → xyχ)
121biimprcd 216 . . . . 5 (ψ → (χφ))
1312ancld 536 . . . 4 (ψ → (χ → (χ φ)))
14132eximdv 1624 . . 3 (ψ → (xyχxy(χ φ)))
1511, 14syl5com 26 . 2 ((A V B W) → (ψxy(χ φ)))
163, 15impbid2 195 1 ((A V B W) → (xy(χ φ) ↔ ψ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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-ext 2334 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-v 2861 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator