Theorem elrabd 3626

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3624. (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

Step	Hyp	Ref	Expression
1		elrabd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		elrabd.3	. 2 ⊢ (𝜑 → 𝜒)
3		elrabd.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
4	3	elrab 3624	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
5	1, 2, 4	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2106  {crab 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434

This theorem is referenced by:  nnawordex  8468  ordtypelem7  9283  oemapvali  9442  rankuni2b  9611  harval2  9755  fin23lem11  10073  fin1a2lem11  10166  pinq  10683  negf1o  11405  uzind4  12646  zsupss  12677  flval3  13535  serge0  13777  expge0  13819  expge1  13820  hashbclem  14164  rlimrege0  15288  lcmgcdlem  16311  phicl2  16469  hashdvds  16476  phisum  16491  pcpremul  16544  prmreclem1  16617  prmreclem3  16619  prmreclem5  16621  ramub  16714  ramub1lem1  16727  ramub1lem2  16728  prmgaplem3  16754  prmgaplem4  16755  prmgaplem5  16756  prmgaplem6  16757  mrcflem  17315  mrcval  17319  isacs1i  17366  coaval  17783  gsumress  18366  issubmd  18445  mhmeql  18464  ghmeql  18857  pmtrval  19059  pmtrrn  19065  symgsssg  19075  symgfisg  19076  psgnunilem5  19102  pgpssslw  19219  efgsfo  19345  oddvdssubg  19456  dprdwd  19614  lmhmeql  20317  cofipsgn  20798  frlmssuvc2  21002  gsumbagdiaglemOLD  21141  gsumbagdiaglem  21144  psrlidm  21172  psrridm  21173  mplmonmul  21237  mhpmulcl  21339  coe1fsupp  21385  dmatmulcl  21649  fctop  22154  cctop  22156  ppttop  22157  pptbas  22158  epttop  22159  ordthauslem  22534  cmpsublem  22550  locfincmp  22677  xkoopn  22740  pthaus  22789  txkgen  22803  xkohaus  22804  xkococnlem  22810  nrmr0reg  22900  fbssfi  22988  filssufilg  23062  uffixsn  23076  ufinffr  23080  ufilen  23081  supnfcls  23171  flimfnfcls  23179  alexsubALTlem4  23201  tmdgsum2  23247  symgtgp  23257  ghmcnp  23266  lmle  24465  iundisj  24712  opnmbllem  24765  vitalilem2  24773  aannenlem2  25489  aalioulem2  25493  radcnv0  25575  jensen  26138  ftalem4  26225  ftalem5  26226  efnnfsumcl  26252  efchtdvds  26308  sqff1o  26331  fsumdvdsdiaglem  26332  dvdsppwf1o  26335  dvdsflf1o  26336  muinv  26342  dchrfi  26403  lgsne0  26483  2lgslem1b  26540  upgr1elem  27482  subumgredg2  27652  subupgr  27654  upgrreslem  27671  umgrreslem  27672  1hevtxdg1  27873  umgr2v2e  27892  pwrssmgc  31278  tocycfv  31376  cycpm3cl2  31403  nsgmgclem  31596  nsgmgc  31597  nsgqusf1olem2  31599  ssmxidllem  31641  ssmxidl  31642  zarcls1  31819  zarclsiin  31821  zart0  31829  ldgenpisyslem1  32131  fmla1  33349  scutbdaybnd  34009  madebdaylemlrcut  34079  cofcut1  34090  cofcutr  34092  aks4d1p5  40088  aks4d1p8  40095  sticksstones2  40103  fnwe2lem2  40876  fnwe2lem3  40877  supminfrnmpt  42985  supminfxr  43004  supminfxr2  43009  supminfxrrnmpt  43011  smflimsuplem5  44357  rabsubmgmd  45345  lubprlem  46256  intubeu  46270  unilbeu  46271