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

Theorem elxp 4305
Description: Membership in a cross product. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
elxp (A (B × 𝐶) ↔ xy(A = ⟨x, y (x B y 𝐶)))
Distinct variable groups:   x,y,A   x,B,y   x,𝐶,y

Proof of Theorem elxp
StepHypRef Expression
1 df-xp 4294 . . 3 (B × 𝐶) = {⟨x, y⟩ ∣ (x B y 𝐶)}
21eleq2i 2101 . 2 (A (B × 𝐶) ↔ A {⟨x, y⟩ ∣ (x B y 𝐶)})
3 elopab 3986 . 2 (A {⟨x, y⟩ ∣ (x B y 𝐶)} ↔ xy(A = ⟨x, y (x B y 𝐶)))
42, 3bitri 173 1 (A (B × 𝐶) ↔ xy(A = ⟨x, y (x B y 𝐶)))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   = wceq 1242  wex 1378   wcel 1390  cop 3370  {copab 3808   × 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-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:  elxp2  4306  0nelxp  4315  0nelelxp  4316  rabxp  4323  elxp3  4337  elvv  4345  elvvv  4346  0xp  4363  xpmlem  4687  elxp4  4751  elxp5  4752  dfco2a  4764  opabex3d  5690  opabex3  5691  xp1st  5734  xp2nd  5735  poxp  5794  xpsnen  6231  xpcomco  6236  xpassen  6240  nqnq0pi  6421
  Copyright terms: Public domain W3C validator