Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rabeqel Structured version   Visualization version   GIF version

Theorem rabeqel 35552
Description: Class element of a restricted class abstraction. (Contributed by Peter Mazsa, 24-Jul-2021.)
Hypotheses
Ref Expression
rabeqel.1 𝐵 = {𝑥𝐴𝜑}
rabeqel.2 (𝑥 = 𝐶 → (𝜑𝜓))
Assertion
Ref Expression
rabeqel (𝐶𝐵 ↔ (𝜓𝐶𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem rabeqel
StepHypRef Expression
1 rabeqel.2 . . 3 (𝑥 = 𝐶 → (𝜑𝜓))
2 rabeqel.1 . . 3 𝐵 = {𝑥𝐴𝜑}
31, 2elrab2 3663 . 2 (𝐶𝐵 ↔ (𝐶𝐴𝜓))
43biancomi 465 1 (𝐶𝐵 ↔ (𝜓𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1537  wcel 2114  {crab 3129
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 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-rab 3134  df-v 3475
This theorem is referenced by:  elrefrels2  35793  elrefrels3  35794  elcnvrefrels2  35806  elcnvrefrels3  35807  elsymrels2  35825  elsymrels3  35826  elsymrels4  35827  elsymrels5  35828  elrefsymrels2  35841  eltrrels2  35851  eltrrels3  35852  eleqvrels2  35863  eleqvrels3  35864  elfunsALTV  35961  eldisjs  35991
  Copyright terms: Public domain W3C validator