Theorem elrabd 3619

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3617. (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 3617	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
5	1, 2, 4	sylanbrc 582	1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424

This theorem is referenced by:  nnawordex  8430  ordtypelem7  9213  oemapvali  9372  rankuni2b  9542  harval2  9686  fin23lem11  10004  fin1a2lem11  10097  pinq  10614  negf1o  11335  uzind4  12575  zsupss  12606  flval3  13463  serge0  13705  expge0  13747  expge1  13748  hashbclem  14092  rlimrege0  15216  lcmgcdlem  16239  phicl2  16397  hashdvds  16404  phisum  16419  pcpremul  16472  prmreclem1  16545  prmreclem3  16547  prmreclem5  16549  ramub  16642  ramub1lem1  16655  ramub1lem2  16656  prmgaplem3  16682  prmgaplem4  16683  prmgaplem5  16684  prmgaplem6  16685  mrcflem  17232  mrcval  17236  isacs1i  17283  coaval  17699  gsumress  18281  issubmd  18360  mhmeql  18379  ghmeql  18772  pmtrval  18974  pmtrrn  18980  symgsssg  18990  symgfisg  18991  psgnunilem5  19017  pgpssslw  19134  efgsfo  19260  oddvdssubg  19371  dprdwd  19529  lmhmeql  20232  cofipsgn  20710  frlmssuvc2  20912  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  psrlidm  21082  psrridm  21083  mplmonmul  21147  mhpmulcl  21249  coe1fsupp  21295  dmatmulcl  21557  fctop  22062  cctop  22064  ppttop  22065  pptbas  22066  epttop  22067  ordthauslem  22442  cmpsublem  22458  locfincmp  22585  xkoopn  22648  pthaus  22697  txkgen  22711  xkohaus  22712  xkococnlem  22718  nrmr0reg  22808  fbssfi  22896  filssufilg  22970  uffixsn  22984  ufinffr  22988  ufilen  22989  supnfcls  23079  flimfnfcls  23087  alexsubALTlem4  23109  tmdgsum2  23155  symgtgp  23165  ghmcnp  23174  lmle  24370  iundisj  24617  opnmbllem  24670  vitalilem2  24678  aannenlem2  25394  aalioulem2  25398  radcnv0  25480  jensen  26043  ftalem4  26130  ftalem5  26131  efnnfsumcl  26157  efchtdvds  26213  sqff1o  26236  fsumdvdsdiaglem  26237  dvdsppwf1o  26240  dvdsflf1o  26241  muinv  26247  dchrfi  26308  lgsne0  26388  2lgslem1b  26445  upgr1elem  27385  subumgredg2  27555  subupgr  27557  upgrreslem  27574  umgrreslem  27575  1hevtxdg1  27776  umgr2v2e  27795  pwrssmgc  31180  tocycfv  31278  cycpm3cl2  31305  nsgmgclem  31498  nsgmgc  31499  nsgqusf1olem2  31501  ssmxidllem  31543  ssmxidl  31544  zarcls1  31721  zarclsiin  31723  zart0  31731  ldgenpisyslem1  32031  fmla1  33249  scutbdaybnd  33936  madebdaylemlrcut  34006  cofcut1  34017  cofcutr  34019  aks4d1p5  40016  aks4d1p8  40023  sticksstones2  40031  fnwe2lem2  40792  fnwe2lem3  40793  supminfrnmpt  42875  supminfxr  42894  supminfxr2  42899  supminfxrrnmpt  42901  smflimsuplem5  44244  rabsubmgmd  45233  lubprlem  46144  intubeu  46158  unilbeu  46159