Theorem opelxp 4317

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	|- ( <.A , B >. e. ( C X. D) <-> (A e. C /\ B e. D))

Proof of Theorem opelxp

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 4306	. 2 |- ( <.A , B >. e. ( C X. D) <-> E.x e. C E.y e. D <.A , B >. = <.x , y >.)
2		vex 2554	. . . . . . 7 |- x e. _V
3		vex 2554	. . . . . . 7 |- y e. _V
4	2, 3	opth2 3968	. . . . . 6 |- ( <.A , B >. = <.x , y >. <-> (A = x /\ B = y))
5		eleq1 2097	. . . . . . 7 |- (A = x -> (A e. C <-> x e. C))
6		eleq1 2097	. . . . . . 7 |- (B = y -> (B e. D <-> y e. D))
7	5, 6	bi2anan9 538	. . . . . 6 |- ((A = x /\ B = y) -> ((A e. C /\ B e. D) <-> (x e. C /\ y e. D)))
8	4, 7	sylbi 114	. . . . 5 |- ( <.A , B >. = <.x , y >. -> ((A e. C /\ B e. D) <-> (x e. C /\ y e. D)))
9	8	biimprcd 149	. . . 4 |- ((x e. C /\ y e. D) -> ( <.A , B >. = <.x , y >. -> (A e. C /\ B e. D)))
10	9	rexlimivv 2432	. . 3 |- (E.x e. C E.y e. D <.A , B >. = <.x , y >. -> (A e. C /\ B e. D))
11		eqid 2037	. . . 4 |- <.A , B >. = <.A , B >.
12		opeq1 3540	. . . . . 6 |- (x = A -> <.x , y >. = <.A , y >.)
13	12	eqeq2d 2048	. . . . 5 |- (x = A -> ( <.A , B >. = <.x , y >. <-> <.A , B >. = <.A , y >.))
14		opeq2 3541	. . . . . 6 |- (y = B -> <.A , y >. = <.A , B >.)
15	14	eqeq2d 2048	. . . . 5 |- (y = B -> ( <.A , B >. = <.A , y >. <-> <.A , B >. = <.A , B >.))
16	13, 15	rspc2ev 2658	. . . 4 |- ((A e. C /\ B e. D /\ <.A , B >. = <.A , B >.) -> E.x e. C E.y e. D <.A , B >. = <.x , y >.)
17	11, 16	mp3an3 1220	. . 3 |- ((A e. C /\ B e. D) -> E.x e. C E.y e. D <.A , B >. = <.x , y >.)
18	10, 17	impbii 117	. 2 |- (E.x e. C E.y e. D <.A , B >. = <.x , y >. <-> (A e. C /\ B e. D))
19	1, 18	bitri 173	1 |- ( <.A , B >. e. ( C X. D) <-> (A e. C /\ B e. D))

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1242   e. wcel 1390  E.wrex 2301   <.cop 3370   X. cxp 4286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294

This theorem is referenced by:  brxp  4318  opelxpi  4319  opelxp1  4320  opelxp2  4321  opthprc  4334  elxp3  4337  opeliunxp  4338  optocl  4359  xpiindim  4416  opelres  4560  resiexg  4596  codir  4656  qfto  4657  xpmlem  4687  rnxpid  4698  ssrnres  4706  dfco2  4763  relssdmrn  4784  ressn  4801  opelf  5005  fnovex  5481  oprab4  5517  resoprab  5539  elmpt2cl  5640  fo1stresm  5730  fo2ndresm  5731  dfoprab4  5760  xporderlem  5793  brecop  6132  xpdom2  6241  enq0enq  6414  enq0sym  6415  enq0tr  6417  nqnq0pi  6421  nnnq0lem1  6429  elinp  6457  genipv  6492  prsrlem1  6670  gt0srpr  6676  opelcn  6725  opelreal  6726  elreal2  6728  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgrom  8877  frecuzrdgsuc  8882