Theorem opelxp 5736

Description: Ordered pair membership in a Cartesian 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.

Step	Hyp	Ref	Expression
1		elxp2 5724	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3492	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3492	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5500	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2832	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2832	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 637	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 217	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 250	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3207	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2740	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4897	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2751	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4898	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2751	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3648	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1450	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 209	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 275	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∃wrex 3076  ⟨cop 4654   × cxp 5698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-opab 5229  df-xp 5706

This theorem is referenced by:  opelxpi  5737  opelxp1  5742  opelxp2  5743  otelxp  5744  otel3xp  5746  brxp  5749  opthprc  5764  elxp3  5766  opeliunxp  5767  bropaex12  5791  optocl  5794  xpsspw  5833  inxp  5856  xpiindi  5860  opelres  6015  restidsing  6082  codir  6152  qfto  6153  xpnz  6190  difxp  6195  xpdifid  6199  dfco2  6276  relssdmrnOLD  6300  ressn  6316  opelf  6782  oprab4  7536  resoprab  7568  oprssdm  7631  nssdmovg  7632  ndmovg  7633  elmpocl  7691  fo1stres  8056  fo2ndres  8057  dfoprab4  8096  opiota  8100  bropopvvv  8131  bropfvvvvlem  8132  curry1  8145  xporderlem  8168  fnwelem  8172  frpoins3xpg  8181  xpord2lem  8183  xpord2pred  8186  xpord2indlem  8188  mpoxopxprcov0  8258  mpocurryd  8310  on2recsov  8724  naddcllem  8732  brecop  8868  brecop2  8869  eceqoveq  8880  xpdom2  9133  mapunen  9212  djuss  9989  djuunxp  9990  dfac5lem2  10193  iunfo  10608  ordpipq  11011  prsrlem1  11141  opelcn  11198  opelreal  11199  elreal2  11201  swrdnznd  14690  swrd00  14692  swrdcl  14693  swrd0  14706  pfx00  14722  pfx0  14723  fsumcom2  15822  fprodcom2  16032  phimullem  16826  imasvscafn  17597  homarcl2  18102  evlfcl  18292  clatl  18578  pzriprnglem4  21518  pzriprnglem9  21523  matplusgcell  22460  iscnp2  23268  txuni2  23594  txcls  23633  txcnpi  23637  txcnp  23649  txcnmpt  23653  txdis1cn  23664  txtube  23669  hausdiag  23674  txlm  23677  tx1stc  23679  txkgen  23681  txflf  24035  tmdcn2  24118  tgphaus  24146  qustgplem  24150  fmucndlem  24321  xmeterval  24463  metustexhalf  24590  blval2  24596  bcthlem1  25377  ovolfcl  25520  ovoliunlem1  25556  mbfimaopnlem  25709  limccnp2  25947  fsumvma  27275  lgsquadlem1  27442  lgsquadlem2  27443  norec2ov  28008  dmrab  32525  xppreima2  32669  aciunf1lem  32680  f1od2  32735  smatrcl  33742  smatlem  33743  qtophaus  33782  eulerpartlemgvv  34341  erdszelem10  35168  cvmlift2lem10  35280  cvmlift2lem12  35282  msubff  35498  elmpst  35504  mpstrcl  35509  elmpps  35541  dfso2  35717  fv1stcnv  35740  fv2ndcnv  35741  txpss3v  35842  dfrdg4  35915  bj-opelrelex  37110  bj-opelidres  37127  bj-elid6  37136  bj-eldiag2  37143  bj-inftyexpitaudisj  37171  curf  37558  curunc  37562  heiborlem3  37773  xrnss3v  38328  inxpxrn  38351  dibopelvalN  41100  dibopelval2  41102  dib1dim  41122  dihopcl  41210  dih1  41243  dih1dimatlem  41286  hdmap1val  41755  aks6d1c3  42080  pellex  42791  elnonrel  43547  mnringmulrcld  44197  fourierdlem42  46070  etransclem44  46199  ovn0lem  46486  ndmaovg  47099  aoprssdm  47117  ndmaovcl  47118  ndmaovrcl  47119  ndmaovcom  47120  ndmaovass  47121  ndmaovdistr  47122  sprsymrelfvlem  47364  sprsymrelfolem2  47367  prproropf1olem2  47378  opeliun2xp  48057  joindm2  48648  meetdm2  48650