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

Theorem elrabd 3633
Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3631. (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 3631 . 2 (𝐴 ∈ {𝑥𝐵𝜓} ↔ (𝐴𝐵𝜒))
51, 2, 4sylanbrc 586 1 (𝜑𝐴 ∈ {𝑥𝐵𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2112  {crab 3113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-rab 3118  df-v 3446
This theorem is referenced by:  nnawordex  8250  ordtypelem7  8976  oemapvali  9135  rankuni2b  9270  harval2  9414  fin23lem11  9732  fin1a2lem11  9825  pinq  10342  negf1o  11063  uzind4  12298  zsupss  12329  flval3  13184  serge0  13424  expge0  13465  expge1  13466  hashbclem  13810  rlimrege0  14932  lcmgcdlem  15944  phicl2  16099  hashdvds  16106  phisum  16121  pcpremul  16174  prmreclem1  16246  prmreclem3  16248  prmreclem5  16250  ramub  16343  ramub1lem1  16356  ramub1lem2  16357  prmgaplem3  16383  prmgaplem4  16384  prmgaplem5  16385  prmgaplem6  16386  mrcflem  16873  mrcval  16877  isacs1i  16924  coaval  17324  gsumress  17888  issubmd  17967  mhmeql  17986  ghmeql  18377  pmtrval  18575  pmtrrn  18581  symgsssg  18591  symgfisg  18592  psgnunilem5  18618  pgpssslw  18735  efgsfo  18861  oddvdssubg  18972  dprdwd  19130  lmhmeql  19824  cofipsgn  20286  frlmssuvc2  20488  gsumbagdiaglem  20617  psrlidm  20645  psrridm  20646  mplmonmul  20708  coe1fsupp  20847  dmatmulcl  21109  fctop  21613  cctop  21615  ppttop  21616  pptbas  21617  epttop  21618  ordthauslem  21992  cmpsublem  22008  locfincmp  22135  xkoopn  22198  pthaus  22247  txkgen  22261  xkohaus  22262  xkococnlem  22268  nrmr0reg  22358  fbssfi  22446  filssufilg  22520  uffixsn  22534  ufinffr  22538  ufilen  22539  supnfcls  22629  flimfnfcls  22637  alexsubALTlem4  22659  tmdgsum2  22705  symgtgp  22715  ghmcnp  22724  lmle  23909  iundisj  24156  opnmbllem  24209  vitalilem2  24217  aannenlem2  24929  aalioulem2  24933  radcnv0  25015  jensen  25578  ftalem4  25665  ftalem5  25666  efnnfsumcl  25692  efchtdvds  25748  sqff1o  25771  fsumdvdsdiaglem  25772  dvdsppwf1o  25775  dvdsflf1o  25776  muinv  25782  dchrfi  25843  lgsne0  25923  2lgslem1b  25980  upgr1elem  26909  subumgredg2  27079  subupgr  27081  upgrreslem  27098  umgrreslem  27099  1hevtxdg1  27300  umgr2v2e  27319  pwrssmgc  30710  tocycfv  30805  cycpm3cl2  30832  ssmxidllem  31053  ssmxidl  31054  zarcls1  31226  zarclsiin  31228  zart0  31236  ldgenpisyslem1  31536  fmla1  32748  fnwe2lem2  39992  fnwe2lem3  39993  supminfrnmpt  42079  supminfxr  42100  supminfxr2  42105  supminfxrrnmpt  42107  smflimsuplem5  43452  rabsubmgmd  44408
  Copyright terms: Public domain W3C validator