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 38255
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 3695 . 2 (𝐶𝐵 ↔ (𝐶𝐴𝜓))
43biancomi 462 1 (𝐶𝐵 ↔ (𝜓𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  {crab 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482
This theorem is referenced by:  elrefrels2  38519  elrefrels3  38520  elcnvrefrels2  38535  elcnvrefrels3  38536  elsymrels2  38554  elsymrels3  38555  elsymrels4  38556  elsymrels5  38557  elrefsymrels2  38570  eltrrels2  38580  eltrrels3  38581  eleqvrels2  38593  eleqvrels3  38594  elfunsALTV  38693  eldisjs  38723
  Copyright terms: Public domain W3C validator