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

Theorem elrabd 3679
Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3677. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypotheses
Ref Expression
elrabd.1 (𝑥 = 𝐴 → (𝜓𝜒))
elrabd.2 (𝜑𝐴𝐵)
elrabd.3 (𝜑𝜒)
Assertion
Ref Expression
elrabd (𝜑𝐴 ∈ {𝑥𝐵𝜓})
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜒,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem elrabd
StepHypRef Expression
1 elrabd.2 . 2 (𝜑𝐴𝐵)
2 elrabd.3 . 2 (𝜑𝜒)
3 elrabd.1 . . 3 (𝑥 = 𝐴 → (𝜓𝜒))
43elrab 3677 . 2 (𝐴 ∈ {𝑥𝐵𝜓} ↔ (𝐴𝐵𝜒))
51, 2, 4sylanbrc 583 1 (𝜑𝐴 ∈ {𝑥𝐵𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  {crab 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494
This theorem is referenced by:  nnawordex  8252  ordtypelem7  8976  oemapvali  9135  rankuni2b  9270  harval2  9414  fin23lem11  9727  fin1a2lem11  9820  pinq  10337  negf1o  11058  fiminreOLD  11578  uzind4  12294  zsupss  12325  flval3  13173  serge0  13412  expge0  13453  expge1  13454  hashbclem  13798  rlimrege0  14924  lcmgcdlem  15938  phicl2  16093  hashdvds  16100  phisum  16115  pcpremul  16168  prmreclem1  16240  prmreclem3  16242  prmreclem5  16244  ramub  16337  ramub1lem1  16350  ramub1lem2  16351  prmgaplem3  16377  prmgaplem4  16378  prmgaplem5  16379  prmgaplem6  16380  mrcflem  16865  mrcval  16869  isacs1i  16916  coaval  17316  gsumress  17880  issubmd  17959  mhmeql  17978  ghmeql  18319  pmtrval  18508  pmtrrn  18514  symgsssg  18524  symgfisg  18525  psgnunilem5  18551  pgpssslw  18668  efgsfo  18794  oddvdssubg  18904  dprdwd  19062  lmhmeql  19756  gsumbagdiaglem  20083  psrlidm  20111  psrridm  20112  mplmonmul  20173  coe1fsupp  20310  cofipsgn  20665  frlmssuvc2  20867  dmatmulcl  21037  fctop  21540  cctop  21542  ppttop  21543  pptbas  21544  epttop  21545  ordthauslem  21919  cmpsublem  21935  locfincmp  22062  xkoopn  22125  pthaus  22174  txkgen  22188  xkohaus  22189  xkococnlem  22195  nrmr0reg  22285  fbssfi  22373  filssufilg  22447  uffixsn  22461  ufinffr  22465  ufilen  22466  supnfcls  22556  flimfnfcls  22564  alexsubALTlem4  22586  tmdgsum2  22632  symgtgp  22637  ghmcnp  22650  lmle  23831  iundisj  24076  opnmbllem  24129  vitalilem2  24137  aannenlem2  24845  aalioulem2  24849  radcnv0  24931  jensen  25493  ftalem4  25580  ftalem5  25581  efnnfsumcl  25607  efchtdvds  25663  sqff1o  25686  fsumdvdsdiaglem  25687  dvdsppwf1o  25690  dvdsflf1o  25691  muinv  25697  dchrfi  25758  lgsne0  25838  2lgslem1b  25895  upgr1elem  26824  subumgredg2  26994  subupgr  26996  upgrreslem  27013  umgrreslem  27014  1hevtxdg1  27215  umgr2v2e  27234  tocycfv  30678  cycpm3cl2  30705  fmla1  32531  fnwe2lem2  39529  fnwe2lem3  39530  supminfrnmpt  41595  supminfxr  41616  supminfxr2  41621  supminfxrrnmpt  41623  smflimsuplem5  42975  rabsubmgmd  43935
  Copyright terms: Public domain W3C validator