Theorem elrabd 3650

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456

This theorem is used by:  fnwe2lem3  8184  fnwe2lem4  8185  nnawordex  8684  cofon1  8719  ordtypelem7  9555  oemapvali  9722  rankuni2b  9904  harval2  10117  fin23lem11  10434  fin1a2lem11  10527  pinq  11051  negf1o  11785  uzind4  13073  zsupss  13104  flval3  13995  serge0  14239  expge0  14281  expge1  14282  hashbclem  14638  rlimrege0  15790  lcmgcdlem  16825  phicl2  16989  hashdvds  16996  phisum  17012  pcpremul  17065  prmreclem1  17138  prmreclem3  17140  prmreclem5  17142  ramub  17235  ramub1lem1  17248  ramub1lem2  17249  prmgaplem3  17275  prmgaplem4  17276  prmgaplem5  17277  prmgaplem6  17278  mrcflem  17830  mrcval  17834  isacs1i  17881  coaval  18293  gsumress  18921  rabsubmgmd  18943  issubmd  19051  mhmeql  19072  ghmeql  19503  pmtrval  19716  pmtrrn  19722  symgsssg  19732  symgfisg  19733  psgnunilem5  19759  pgpssslw  19879  efgsfo  20004  oddvdssubg  20120  dprdwd  20278  lmhmeql  21381  ssdifidllem  21691  ssdifidl  21692  cofipsgn  21954  frlmssuvc2  22156  gsumbagdiaglem  22294  psrlidm  22324  psrridm  22325  mplmonmul  22400  mhpmulcl  22525  psdmul  22542  coe1fsupp  22587  dmatmulcl  22870  fctop  23377  cctop  23379  ppttop  23380  pptbas  23381  epttop  23382  ordthauslem  23756  cmpsublem  23772  locfincmp  23900  xkoopn  23963  pthaus  24012  txkgen  24026  xkohaus  24027  xkococnlem  24033  nrmr0reg  24123  fbssfi  24211  filssufilg  24285  uffixsn  24299  ufinffr  24303  ufilen  24304  supnfcls  24394  flimfnfcls  24402  alexsubALTlem4  24424  tmdgsum2  24470  symgtgp  24480  ghmcnp  24489  lmle  25677  iundisj  25924  opnmbllem  25977  vitalilem2  25985  aannenlem2  26713  aalioulem2  26717  radcnv0  26800  jensen  27373  ftalem4  27460  ftalem5  27461  efnnfsumcl  27487  efchtdvds  27543  sqff1o  27566  fsumdvdsdiaglem  27567  dvdsppwf1o  27570  dvdsflf1o  27571  muinv  27577  dchrfi  27639  lgsne0  27719  2lgslem1b  27776  cutbdaybnd  28238  madebdaylemlrcut  28342  sltsbday  28360  cofcut1  28363  cofcutr  28367  noseqinds  28736  onsfi  28799  elcgrabasrd  29433  cgrabasimass  29435  upgr1elem  29747  subumgredg2  29923  subupgr  29925  upgrreslem  29942  umgrreslem  29943  1hevtxdg1  30144  umgr2v2e  30163  pwrssmgc  33660  tocycfv  33769  cycpm3cl2  33796  elrgspnlem1  33902  elrgspnlem2  33903  elrgspnlem3  33904  elrgspnlem4  33905  elrgspnsubrunlem1  33907  fldgensdrg  33980  fldgenssv  33981  fldgenssp  33984  nsgmgclem  34066  nsgmgc  34067  nsgqusf1olem2  34069  ssmxidllem  34102  ssmxidl  34103  1arithufdlem1  34180  1arithufdlem2  34181  1arithufdlem3  34182  1arithufdlem4  34183  0mplrim  34257  selvply1rhmlema  34261  selvply1rhmlemb  34262  selvply1rhmlem1  34263  selvply1rhmlem2  34264  selvply1rhmlem4  34266  selvply1rhm0  34269  extvfvvcl  34278  extvfvcl  34279  mplmulmvr  34282  evlextv  34285  mplvrpmlem  34286  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmmhm  34289  mplvrpmrhm  34290  psrmonmul  34293  psrmonprod  34295  esplyfval0  34307  esplylem  34309  esplyfv1  34312  esplyfvaln  34317  esplyind  34318  minplymindeg  34451  minplyirredlem  34453  irngnminplynz  34455  irredminply  34459  zarcls1  34612  zarclsiin  34614  zart0  34622  ldgenpisyslem1  34907  fmla1  36360  aks4d1p5  43396  aks4d1p8  43403  primrootsunit1  43413  primrootscoprmpow  43415  primrootscoprbij  43418  hashscontpow1  43437  sticksstones2  43463  grpods  43510  unitscyglem1  43511  unitscyglem2  43512  unitscyglem4  43514  supinf  43560  onintunirab  44490  naddwordnexlem4  44664  supminfrnmpt  46728  supminfxr  46747  supminfxr2  46752  supminfxrrnmpt  46754  sumnnodd  46915  dvnprodlem1  47229  smflimsuplem5  48107  tmachlem-agreeself  48219  lubprlem  50407  intubeu  50429  unilbeu  50430