Theorem opelxp 5687

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 5675	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
2		vex 3455	. . . . . . 7 ⊢ 𝑥 ∈ V
3		vex 3455	. . . . . . 7 ⊢ 𝑦 ∈ V
4	2, 3	opth2 5449	. . . . . 6 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 = 𝑥 ∧ 𝐵 = 𝑦))
5		eleq1 2849	. . . . . . 7 ⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶))
6		eleq1 2849	. . . . . . 7 ⊢ (𝐵 = 𝑦 → (𝐵 ∈ 𝐷 ↔ 𝑦 ∈ 𝐷))
7	5, 6	bi2anan9 650	. . . . . 6 ⊢ ((𝐴 = 𝑥 ∧ 𝐵 = 𝑦) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
8	4, 7	sylbi 220	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷)))
9	8	biimprcd 253	. . . 4 ⊢ ((𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐷) → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)))
10	9	rexlimivv 3205	. . 3 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
11		eqid 2761	. . . 4 ⊢ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩
12		opeq1 4833	. . . . . 6 ⊢ (𝑥 = 𝐴 → ⟨𝑥, 𝑦⟩ = ⟨𝐴, 𝑦⟩)
13	12	eqeq2d 2772	. . . . 5 ⊢ (𝑥 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩))
14		opeq2 4834	. . . . . 6 ⊢ (𝑦 = 𝐵 → ⟨𝐴, 𝑦⟩ = ⟨𝐴, 𝐵⟩)
15	14	eqeq2d 2772	. . . . 5 ⊢ (𝑦 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑦⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
16	13, 15	rspc2ev 3589	. . . 4 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
17	11, 16	mp3an3 1479	. . 3 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩)
18	10, 17	impbii 212	. 2 ⊢ (∃𝑥 ∈ 𝐶 ∃𝑦 ∈ 𝐷 ⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))
19	1, 18	bitri 278	1 ⊢ (⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃wrex 3087  ⟨cop 4590   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-xp 5657

This theorem is used by:  opelxpi  5688  opelxp1  5693  opelxp2  5694  otelxp  5695  otel3xp  5697  brxp  5700  opthprc  5715  elxp3  5717  opeliunxp  5718  opeliun2xp  5719  bropaex12  5742  optoclOLD  5746  xpsspw  5787  inxp  5809  xpiindi  5812  opelres  5976  restidsing  6045  codir  6114  qfto  6115  xpnz  6150  difxp  6155  xpdifid  6159  xpdifcnvepel  6160  dfco2  6246  ressn  6288  opelf  6743  oprab4  7506  resoprab  7538  oprssdm  7602  nssdmovg  7603  ndmovg  7604  elmpocl  7662  fo1stres  8027  fo2ndres  8028  dfoprab4  8066  opiota  8070  bropopvvv  8101  bropfvvvvlem  8102  curry1  8115  xporderlem  8139  fnwelem  8143  frpoins3xpg  8157  xpord2lem  8159  xpord2pred  8162  xpord2indlem  8164  mpoxopxprcov0  8234  mpocurryd  8286  on2recsov  8677  naddcllem  8685  brecop  8831  brecop2  8832  eceqoveq  8843  curf  8890  xpdom2  9091  mapunen  9165  djuss  10001  djuunxp  10002  dfac5lem2  10203  iunfo  10623  ordpipq  11027  prsrlem1  11157  opelcn  11214  opelreal  11215  elreal2  11217  swrdnznd  14790  swrd00  14792  swrdcl  14793  swrd0  14808  pfx00  14824  pfx0  14825  fsumcom2  15940  fprodcom2  16151  phimullem  16956  imasvscafn  17709  homarcl2  18210  evlfcl  18396  clatl  18682  pzriprnglem4  21790  pzriprnglem9  21795  matplusgcell  22748  iscnp2  23557  txuni2  23884  txcls  23923  txcnpi  23927  txcnp  23939  txcnmpt  23943  txdis1cn  23954  txtube  23959  hausdiag  23964  txlm  23967  tx1stc  23969  txkgen  23971  txflf  24325  tmdcn2  24408  tgphaus  24436  qustgplem  24440  fmucndlem  24609  xmeterval  24751  metustexhalf  24875  blval2  24881  bcthlem1  25645  ovolfcl  25787  ovoliunlem1  25823  mbfimaopnlem  25976  limccnp2  26212  fsumvma  27540  lgsquadlem1  27707  lgsquadlem2  27708  norec2ov  28343  dmrab  33093  xppreima2  33245  aciunf1lem  33256  f1od2  33311  smatrcl  34428  smatlem  34429  qtophaus  34468  eulerpartlemgvv  35008  erdszelem10  35965  cvmlift2lem10  36077  cvmlift2lem12  36079  msubff  36295  elmpst  36301  mpstrcl  36306  elmpps  36338  dfso2  36520  fv1stcnv  36541  fv2ndcnv  36542  txpss3v  36640  dfrdg4  36715  bj-opelrelex  38065  bj-opelidres  38082  bj-elid6  38091  bj-eldiag2  38098  bj-inftyexpitaudisj  38126  curunc  38525  heiborlem3  38747  xrnss3v  39313  ecxrn2  39340  inxpxrn  39350  dibopelvalN  42200  dibopelval2  42202  dib1dim  42222  dihopcl  42310  dih1  42343  dih1dimatlem  42386  hdmap1val  42855  aks6d1c3  43173  pellex  43841  elnonrel  44585  mnringmulrcld  45225  fourierdlem42  47158  etransclem44  47287  ovn0lem  47574  ndmaovg  48253  aoprssdm  48271  ndmaovcl  48272  ndmaovrcl  48273  ndmaovcom  48274  ndmaovass  48275  ndmaovdistr  48276  sprsymrelfvlem  48571  sprsymrelfolem2  48574  prproropf1olem2  48585  opgpgvtx  49152  iinxp  49940  coxp  49942  joindm2  50075  meetdm2  50077  swapf2fval  50372  swapf1val  50374  fuco2el  50419