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

Theorem elrabd 3645
Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3643. (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 3643 . 2 (𝐴 ∈ {𝑥𝐵𝜓} ↔ (𝐴𝐵𝜒))
51, 2, 4sylanbrc 583 1 (𝜑𝐴 ∈ {𝑥𝐵𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  {crab 3405
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445
This theorem is referenced by:  nnawordex  8580  cofon1  8614  ordtypelem7  9456  oemapvali  9616  rankuni2b  9785  harval2  9929  fin23lem11  10249  fin1a2lem11  10342  pinq  10859  negf1o  11581  uzind4  12823  zsupss  12854  flval3  13712  serge0  13954  expge0  13996  expge1  13997  hashbclem  14341  rlimrege0  15453  lcmgcdlem  16474  phicl2  16632  hashdvds  16639  phisum  16654  pcpremul  16707  prmreclem1  16780  prmreclem3  16782  prmreclem5  16784  ramub  16877  ramub1lem1  16890  ramub1lem2  16891  prmgaplem3  16917  prmgaplem4  16918  prmgaplem5  16919  prmgaplem6  16920  mrcflem  17478  mrcval  17482  isacs1i  17529  coaval  17946  gsumress  18529  issubmd  18609  mhmeql  18628  ghmeql  19022  pmtrval  19224  pmtrrn  19230  symgsssg  19240  symgfisg  19241  psgnunilem5  19267  pgpssslw  19387  efgsfo  19512  oddvdssubg  19624  dprdwd  19781  lmhmeql  20501  cofipsgn  20982  frlmssuvc2  21186  gsumbagdiaglemOLD  21325  gsumbagdiaglem  21328  psrlidm  21356  psrridm  21357  mplmonmul  21421  mhpmulcl  21523  coe1fsupp  21569  dmatmulcl  21833  fctop  22338  cctop  22340  ppttop  22341  pptbas  22342  epttop  22343  ordthauslem  22718  cmpsublem  22734  locfincmp  22861  xkoopn  22924  pthaus  22973  txkgen  22987  xkohaus  22988  xkococnlem  22994  nrmr0reg  23084  fbssfi  23172  filssufilg  23246  uffixsn  23260  ufinffr  23264  ufilen  23265  supnfcls  23355  flimfnfcls  23363  alexsubALTlem4  23385  tmdgsum2  23431  symgtgp  23441  ghmcnp  23450  lmle  24649  iundisj  24896  opnmbllem  24949  vitalilem2  24957  aannenlem2  25673  aalioulem2  25677  radcnv0  25759  jensen  26322  ftalem4  26409  ftalem5  26410  efnnfsumcl  26436  efchtdvds  26492  sqff1o  26515  fsumdvdsdiaglem  26516  dvdsppwf1o  26519  dvdsflf1o  26520  muinv  26526  dchrfi  26587  lgsne0  26667  2lgslem1b  26724  scutbdaybnd  27138  madebdaylemlrcut  27212  cofcut1  27223  cofcutr  27227  upgr1elem  27949  subumgredg2  28119  subupgr  28121  upgrreslem  28138  umgrreslem  28139  1hevtxdg1  28340  umgr2v2e  28359  pwrssmgc  31743  tocycfv  31841  cycpm3cl2  31868  fldgensdrg  31966  fldgenid  31969  nsgmgclem  32072  nsgmgc  32073  nsgqusf1olem2  32075  ssmxidllem  32117  ssmxidl  32118  zarcls1  32319  zarclsiin  32321  zart0  32329  ldgenpisyslem1  32631  fmla1  33850  aks4d1p5  40504  aks4d1p8  40511  sticksstones2  40522  fnwe2lem2  41316  fnwe2lem3  41317  onintunirab  41499  supminfrnmpt  43616  supminfxr  43635  supminfxr2  43640  supminfxrrnmpt  43642  smflimsuplem5  44997  rabsubmgmd  46017  lubprlem  46927  intubeu  46941  unilbeu  46942
  Copyright terms: Public domain W3C validator