Theorem opelxp 5591

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 5579	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3497	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3497	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5372	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2900	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2900	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 637	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 219	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 252	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3292	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2821	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4803	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2832	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4804	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2832	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3635	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1446	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 211	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 277	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

Syntax hints:   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃wrex 3139  ⟨cop 4573   × cxp 5553

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5129  df-xp 5561

This theorem is referenced by:  opelxpi  5592  opelxp1  5596  opelxp2  5597  otel3xp  5599  brxp  5601  opthprc  5616  elxp3  5618  opeliunxp  5619  bropaex12  5642  optocl  5645  xpsspw  5682  xpiindi  5706  opelres  5859  restidsing  5922  codir  5980  qfto  5981  xpnz  6016  difxp  6021  xpdifid  6025  dfco2  6098  relssdmrn  6121  ressn  6136  opelf  6539  oprab4  7240  resoprab  7270  oprssdm  7329  nssdmovg  7330  ndmovg  7331  elmpocl  7387  fo1stres  7715  fo2ndres  7716  dfoprab4  7753  opiota  7757  bropopvvv  7785  bropfvvvvlem  7786  curry1  7799  xporderlem  7821  fnwelem  7825  mpoxopxprcov0  7883  mpocurryd  7935  brecop  8390  brecop2  8391  eceqoveq  8402  xpdom2  8612  mapunen  8686  djuss  9349  djuunxp  9350  dfac5lem2  9550  iunfo  9961  ordpipq  10364  prsrlem1  10494  opelcn  10551  opelreal  10552  elreal2  10554  swrdnznd  14004  swrd00  14006  swrdcl  14007  swrd0  14020  pfx00  14036  pfx0  14037  fsumcom2  15129  fprodcom2  15338  phimullem  16116  imasvscafn  16810  homarcl2  17295  evlfcl  17472  clatl  17726  matplusgcell  21042  iscnp2  21847  txuni2  22173  txcls  22212  txcnpi  22216  txcnp  22228  txcnmpt  22232  txdis1cn  22243  txtube  22248  hausdiag  22253  txlm  22256  tx1stc  22258  txkgen  22260  txflf  22614  tmdcn2  22697  tgphaus  22725  qustgplem  22729  fmucndlem  22900  xmeterval  23042  metustexhalf  23166  blval2  23172  bcthlem1  23927  ovolfcl  24067  ovoliunlem1  24103  mbfimaopnlem  24256  limccnp2  24490  fsumvma  25789  lgsquadlem1  25956  lgsquadlem2  25957  dmrab  30260  xppreima2  30395  aciunf1lem  30407  f1od2  30457  smatrcl  31061  smatlem  31062  qtophaus  31100  eulerpartlemgvv  31634  erdszelem10  32447  cvmlift2lem10  32559  cvmlift2lem12  32561  msubff  32777  elmpst  32783  mpstrcl  32788  elmpps  32820  dfso2  32990  fv1stcnv  33020  fv2ndcnv  33021  txpss3v  33339  dfrdg4  33412  bj-opelrelex  34439  bj-opelidres  34456  bj-elid6  34465  bj-eldiag2  34472  bj-inftyexpitaudisj  34490  curf  34885  curunc  34889  heiborlem3  35106  xrnss3v  35639  inxpxrn  35658  dibopelvalN  38294  dibopelval2  38296  dib1dim  38316  dihopcl  38404  dih1  38437  dih1dimatlem  38480  hdmap1val  38949  pellex  39481  elnonrel  39994  fourierdlem42  42483  etransclem44  42612  ovn0lem  42896  ndmaovg  43432  aoprssdm  43450  ndmaovcl  43451  ndmaovrcl  43452  ndmaovcom  43453  ndmaovass  43454  ndmaovdistr  43455  sprsymrelfvlem  43701  sprsymrelfolem2  43704  prproropf1olem2  43715  opeliun2xp  44430