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

Theorem preq12bg 4128
 Description: Closed form of preq12b 4127. (Contributed by Scott Fenton, 28-Mar-2014.)
Assertion
Ref Expression
preq12bg (((A V B W) (C X D Y)) → ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C))))

Proof of Theorem preq12bg
Dummy variables x y z w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 preq1 3799 . . . . . . 7 (x = A → {x, y} = {A, y})
21eqeq1d 2361 . . . . . 6 (x = A → ({x, y} = {z, D} ↔ {A, y} = {z, D}))
3 eqeq1 2359 . . . . . . . 8 (x = A → (x = zA = z))
43anbi1d 685 . . . . . . 7 (x = A → ((x = z y = D) ↔ (A = z y = D)))
5 eqeq1 2359 . . . . . . . 8 (x = A → (x = DA = D))
65anbi1d 685 . . . . . . 7 (x = A → ((x = D y = z) ↔ (A = D y = z)))
74, 6orbi12d 690 . . . . . 6 (x = A → (((x = z y = D) (x = D y = z)) ↔ ((A = z y = D) (A = D y = z))))
82, 7bibi12d 312 . . . . 5 (x = A → (({x, y} = {z, D} ↔ ((x = z y = D) (x = D y = z))) ↔ ({A, y} = {z, D} ↔ ((A = z y = D) (A = D y = z)))))
98imbi2d 307 . . . 4 (x = A → ((D Y → ({x, y} = {z, D} ↔ ((x = z y = D) (x = D y = z)))) ↔ (D Y → ({A, y} = {z, D} ↔ ((A = z y = D) (A = D y = z))))))
10 preq2 3800 . . . . . . 7 (y = B → {A, y} = {A, B})
1110eqeq1d 2361 . . . . . 6 (y = B → ({A, y} = {z, D} ↔ {A, B} = {z, D}))
12 eqeq1 2359 . . . . . . . 8 (y = B → (y = DB = D))
1312anbi2d 684 . . . . . . 7 (y = B → ((A = z y = D) ↔ (A = z B = D)))
14 eqeq1 2359 . . . . . . . 8 (y = B → (y = zB = z))
1514anbi2d 684 . . . . . . 7 (y = B → ((A = D y = z) ↔ (A = D B = z)))
1613, 15orbi12d 690 . . . . . 6 (y = B → (((A = z y = D) (A = D y = z)) ↔ ((A = z B = D) (A = D B = z))))
1711, 16bibi12d 312 . . . . 5 (y = B → (({A, y} = {z, D} ↔ ((A = z y = D) (A = D y = z))) ↔ ({A, B} = {z, D} ↔ ((A = z B = D) (A = D B = z)))))
1817imbi2d 307 . . . 4 (y = B → ((D Y → ({A, y} = {z, D} ↔ ((A = z y = D) (A = D y = z)))) ↔ (D Y → ({A, B} = {z, D} ↔ ((A = z B = D) (A = D B = z))))))
19 preq1 3799 . . . . . . 7 (z = C → {z, D} = {C, D})
2019eqeq2d 2364 . . . . . 6 (z = C → ({A, B} = {z, D} ↔ {A, B} = {C, D}))
21 eqeq2 2362 . . . . . . . 8 (z = C → (A = zA = C))
2221anbi1d 685 . . . . . . 7 (z = C → ((A = z B = D) ↔ (A = C B = D)))
23 eqeq2 2362 . . . . . . . 8 (z = C → (B = zB = C))
2423anbi2d 684 . . . . . . 7 (z = C → ((A = D B = z) ↔ (A = D B = C)))
2522, 24orbi12d 690 . . . . . 6 (z = C → (((A = z B = D) (A = D B = z)) ↔ ((A = C B = D) (A = D B = C))))
2620, 25bibi12d 312 . . . . 5 (z = C → (({A, B} = {z, D} ↔ ((A = z B = D) (A = D B = z))) ↔ ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C)))))
2726imbi2d 307 . . . 4 (z = C → ((D Y → ({A, B} = {z, D} ↔ ((A = z B = D) (A = D B = z)))) ↔ (D Y → ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C))))))
28 preq2 3800 . . . . . . 7 (w = D → {z, w} = {z, D})
2928eqeq2d 2364 . . . . . 6 (w = D → ({x, y} = {z, w} ↔ {x, y} = {z, D}))
30 eqeq2 2362 . . . . . . . 8 (w = D → (y = wy = D))
3130anbi2d 684 . . . . . . 7 (w = D → ((x = z y = w) ↔ (x = z y = D)))
32 eqeq2 2362 . . . . . . . 8 (w = D → (x = wx = D))
3332anbi1d 685 . . . . . . 7 (w = D → ((x = w y = z) ↔ (x = D y = z)))
3431, 33orbi12d 690 . . . . . 6 (w = D → (((x = z y = w) (x = w y = z)) ↔ ((x = z y = D) (x = D y = z))))
35 vex 2862 . . . . . . 7 x V
36 vex 2862 . . . . . . 7 y V
37 vex 2862 . . . . . . 7 z V
38 vex 2862 . . . . . . 7 w V
3935, 36, 37, 38preq12b 4127 . . . . . 6 ({x, y} = {z, w} ↔ ((x = z y = w) (x = w y = z)))
4029, 34, 39vtoclbg 2915 . . . . 5 (D Y → ({x, y} = {z, D} ↔ ((x = z y = D) (x = D y = z))))
4140a1i 10 . . . 4 ((x V y W z X) → (D Y → ({x, y} = {z, D} ↔ ((x = z y = D) (x = D y = z)))))
429, 18, 27, 41vtocl3ga 2924 . . 3 ((A V B W C X) → (D Y → ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C)))))
43423expa 1151 . 2 (((A V B W) C X) → (D Y → ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C)))))
4443impr 602 1 (((A V B W) (C X D Y)) → ({A, B} = {C, D} ↔ ((A = C B = D) (A = D B = C))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358   ∧ w3a 934   = wceq 1642   ∈ wcel 1710  {cpr 3738 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-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-nin 3211  df-compl 3212  df-un 3214  df-sn 3741  df-pr 3742 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator