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

Theorem opelxp 4581
 Description: Ordered pair membership in a cross product. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opelxp (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))

Proof of Theorem opelxp
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp2 4569 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2 vex 2694 . . . . . . 7 𝑥 ∈ V
3 vex 2694 . . . . . . 7 𝑦 ∈ V
42, 3opth2 4173 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥𝐵 = 𝑦))
5 eleq1 2204 . . . . . . 7 (𝐴 = 𝑥 → (𝐴𝐶𝑥𝐶))
6 eleq1 2204 . . . . . . 7 (𝐵 = 𝑦 → (𝐵𝐷𝑦𝐷))
75, 6bi2anan9 596 . . . . . 6 ((𝐴 = 𝑥𝐵 = 𝑦) → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
84, 7sylbi 120 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
98biimprcd 159 . . . 4 ((𝑥𝐶𝑦𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷)))
109rexlimivv 2560 . . 3 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷))
11 eqid 2141 . . . 4 𝐴, 𝐵⟩ = ⟨𝐴, 𝐵
12 opeq1 3715 . . . . . 6 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
1312eqeq2d 2153 . . . . 5 (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14 opeq2 3716 . . . . . 6 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1514eqeq2d 2153 . . . . 5 (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
1613, 15rspc2ev 2810 . . . 4 ((𝐴𝐶𝐵𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1711, 16mp3an3 1305 . . 3 ((𝐴𝐶𝐵𝐷) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1810, 17impbii 125 . 2 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴𝐶𝐵𝐷))
191, 18bitri 183 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 1481  ∃wrex 2419  ⟨cop 3537   × cxp 4549 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2123  ax-sep 4056  ax-pow 4108  ax-pr 4142 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1738  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ral 2423  df-rex 2424  df-v 2693  df-un 3082  df-in 3084  df-ss 3091  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-opab 4000  df-xp 4557 This theorem is referenced by:  brxp  4582  opelxpi  4583  opelxp1  4585  opelxp2  4586  opthprc  4602  elxp3  4605  opeliunxp  4606  optocl  4627  xpiindim  4688  opelres  4836  resiexg  4876  codir  4939  qfto  4940  xpmlem  4971  rnxpid  4985  ssrnres  4993  dfco2  5050  relssdmrn  5071  ressn  5091  opelf  5306  fnovex  5816  oprab4  5854  resoprab  5879  elmpocl  5980  fo1stresm  6071  fo2ndresm  6072  dfoprab4  6102  xporderlem  6140  f1od2  6144  brecop  6531  xpdom2  6737  djulclb  6957  djuss  6972  enq0enq  7292  enq0sym  7293  enq0tr  7295  nqnq0pi  7299  nnnq0lem1  7307  elinp  7335  genipv  7370  prsrlem1  7603  gt0srpr  7609  opelcn  7687  opelreal  7688  elreal2  7691  frecuzrdgrrn  10241  frec2uzrdg  10242  frecuzrdgrcl  10243  frecuzrdgsuc  10247  frecuzrdgrclt  10248  frecuzrdgsuctlem  10256  fisumcom2  11268  sqpweven  11925  2sqpwodd  11926  phimullem  11973  txuni2  12500  txcnp  12515  txcnmpt  12517  txdis1cn  12522  txlm  12523  xmeterval  12679  limccnp2lem  12889  limccnp2cntop  12890
 Copyright terms: Public domain W3C validator