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

Theorem opelxp 4671
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 4659 . 2 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2 vex 2755 . . . . . . 7 𝑥 ∈ V
3 vex 2755 . . . . . . 7 𝑦 ∈ V
42, 3opth2 4255 . . . . . 6 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥𝐵 = 𝑦))
5 eleq1 2252 . . . . . . 7 (𝐴 = 𝑥 → (𝐴𝐶𝑥𝐶))
6 eleq1 2252 . . . . . . 7 (𝐵 = 𝑦 → (𝐵𝐷𝑦𝐷))
75, 6bi2anan9 606 . . . . . 6 ((𝐴 = 𝑥𝐵 = 𝑦) → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
84, 7sylbi 121 . . . . 5 (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴𝐶𝐵𝐷) ↔ (𝑥𝐶𝑦𝐷)))
98biimprcd 160 . . . 4 ((𝑥𝐶𝑦𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷)))
109rexlimivv 2613 . . 3 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴𝐶𝐵𝐷))
11 eqid 2189 . . . 4 𝐴, 𝐵⟩ = ⟨𝐴, 𝐵
12 opeq1 3793 . . . . . 6 (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
1312eqeq2d 2201 . . . . 5 (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14 opeq2 3794 . . . . . 6 (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
1514eqeq2d 2201 . . . . 5 (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
1613, 15rspc2ev 2871 . . . 4 ((𝐴𝐶𝐵𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1711, 16mp3an3 1337 . . 3 ((𝐴𝐶𝐵𝐷) → ∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
1810, 17impbii 126 . 2 (∃𝑥𝐶𝑦𝐷𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴𝐶𝐵𝐷))
191, 18bitri 184 1 (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105   = wceq 1364  wcel 2160  wrex 2469  cop 3610   × cxp 4639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224
This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-rex 2474  df-v 2754  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-opab 4080  df-xp 4647
This theorem is referenced by:  brxp  4672  opelxpi  4673  opelxp1  4675  opelxp2  4676  opthprc  4692  elxp3  4695  opeliunxp  4696  optocl  4717  xpiindim  4779  opelres  4927  resiexg  4967  restidsing  4978  codir  5032  qfto  5033  xpmlem  5064  rnxpid  5078  ssrnres  5086  dfco2  5143  relssdmrn  5164  ressn  5184  opelf  5403  fnovex  5925  oprab4  5963  resoprab  5988  elmpocl  6087  fo1stresm  6181  fo2ndresm  6182  dfoprab4  6212  xporderlem  6251  f1od2  6255  brecop  6646  xpdom2  6852  djulclb  7079  djuss  7094  enq0enq  7455  enq0sym  7456  enq0tr  7458  nqnq0pi  7462  nnnq0lem1  7470  elinp  7498  genipv  7533  prsrlem1  7766  gt0srpr  7772  opelcn  7850  opelreal  7851  elreal2  7854  frecuzrdgrrn  10434  frec2uzrdg  10435  frecuzrdgrcl  10436  frecuzrdgsuc  10440  frecuzrdgrclt  10441  frecuzrdgsuctlem  10449  fisumcom2  11473  fprodcom2fi  11661  sqpweven  12202  2sqpwodd  12203  phimullem  12252  txuni2  14193  txcnp  14208  txcnmpt  14210  txdis1cn  14215  txlm  14216  xmeterval  14372  limccnp2lem  14582  limccnp2cntop  14583
  Copyright terms: Public domain W3C validator