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 38236
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 3698 . 2 (𝐶𝐵 ↔ (𝐶𝐴𝜓))
43biancomi 462 1 (𝐶𝐵 ↔ (𝜓𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wcel 2106  {crab 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480
This theorem is referenced by:  elrefrels2  38500  elrefrels3  38501  elcnvrefrels2  38516  elcnvrefrels3  38517  elsymrels2  38535  elsymrels3  38536  elsymrels4  38537  elsymrels5  38538  elrefsymrels2  38551  eltrrels2  38561  eltrrels3  38562  eleqvrels2  38574  eleqvrels3  38575  elfunsALTV  38674  eldisjs  38704
  Copyright terms: Public domain W3C validator