MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brab2a Structured version   Visualization version   GIF version

Theorem brab2a 5730
Description: The law of concretion for a binary relation. Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 28-Apr-2015.)
Hypotheses
Ref Expression
brab2a.1 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
brab2a.2 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)}
Assertion
Ref Expression
brab2a (𝐴𝑅𝐵 ↔ ((𝐴𝐶𝐵𝐷) ∧ 𝜓))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝜓,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑅(𝑥,𝑦)

Proof of Theorem brab2a
StepHypRef Expression
1 brab2a.2 . . . 4 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)}
2 opabssxp 5729 . . . 4 {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)} ⊆ (𝐶 × 𝐷)
31, 2eqsstri 3983 . . 3 𝑅 ⊆ (𝐶 × 𝐷)
43brel 5702 . 2 (𝐴𝑅𝐵 → (𝐴𝐶𝐵𝐷))
5 df-br 5111 . . . 4 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
61eleq2i 2830 . . . 4 (⟨𝐴, 𝐵⟩ ∈ 𝑅 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)})
75, 6bitri 275 . . 3 (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)})
8 brab2a.1 . . . 4 ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))
98opelopab2a 5497 . . 3 ((𝐴𝐶𝐵𝐷) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)} ↔ 𝜓))
107, 9bitrid 283 . 2 ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝜓))
114, 10biadanii 821 1 (𝐴𝑅𝐵 ↔ ((𝐴𝐶𝐵𝐷) ∧ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  cop 4597   class class class wbr 5110  {copab 5172   × cxp 5636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644
This theorem is referenced by:  fnse  8070  ltxrlt  11232  ltxr  13043  issect  17643  gaorb  19094  ispgp  19381  efgcpbllema  19543  lmbr  22625  isphtpc  24373  vitalilem1  24988  vitalilem2  24989  vitalilem3  24990  tgjustf  27457  iscgrg  27496  ishlg  27586  iscgra  27793  isinag  27822  isleag  27831  mgcval  31889  filnetlem1  34879  bj-brab2a1  35649  prjsprel  40971
  Copyright terms: Public domain W3C validator