Theorem elrabd 3646

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452

This theorem is used by:  fnwe2lem3  8150  fnwe2lem4  8151  nnawordex  8650  cofon1  8685  ordtypelem7  9522  oemapvali  9689  rankuni2b  9871  harval2  10082  fin23lem11  10399  fin1a2lem11  10492  pinq  11016  negf1o  11750  uzind4  13037  zsupss  13068  flval3  13959  serge0  14203  expge0  14245  expge1  14246  hashbclem  14601  rlimrege0  15752  lcmgcdlem  16787  phicl2  16951  hashdvds  16958  phisum  16974  pcpremul  17027  prmreclem1  17100  prmreclem3  17102  prmreclem5  17104  ramub  17197  ramub1lem1  17210  ramub1lem2  17211  prmgaplem3  17237  prmgaplem4  17238  prmgaplem5  17239  prmgaplem6  17240  mrcflem  17786  mrcval  17790  isacs1i  17837  coaval  18249  gsumress  18877  rabsubmgmd  18899  issubmd  19007  mhmeql  19028  ghmeql  19459  pmtrval  19671  pmtrrn  19677  symgsssg  19687  symgfisg  19688  psgnunilem5  19714  pgpssslw  19834  efgsfo  19959  oddvdssubg  20075  dprdwd  20233  lmhmeql  21336  ssdifidllem  21646  ssdifidl  21647  cofipsgn  21905  frlmssuvc2  22107  gsumbagdiaglem  22245  psrlidm  22275  psrridm  22276  mplmonmul  22351  mhpmulcl  22476  psdmul  22493  coe1fsupp  22538  dmatmulcl  22821  fctop  23328  cctop  23330  ppttop  23331  pptbas  23332  epttop  23333  ordthauslem  23707  cmpsublem  23723  locfincmp  23851  xkoopn  23914  pthaus  23963  txkgen  23977  xkohaus  23978  xkococnlem  23984  nrmr0reg  24074  fbssfi  24162  filssufilg  24236  uffixsn  24250  ufinffr  24254  ufilen  24255  supnfcls  24345  flimfnfcls  24353  alexsubALTlem4  24375  tmdgsum2  24421  symgtgp  24431  ghmcnp  24440  lmle  25628  iundisj  25875  opnmbllem  25928  vitalilem2  25936  aannenlem2  26662  aalioulem2  26666  radcnv0  26749  jensen  27322  ftalem4  27409  ftalem5  27410  efnnfsumcl  27436  efchtdvds  27492  sqff1o  27515  fsumdvdsdiaglem  27516  dvdsppwf1o  27519  dvdsflf1o  27520  muinv  27526  dchrfi  27588  lgsne0  27668  2lgslem1b  27725  cutbdaybnd  28187  madebdaylemlrcut  28291  sltsbday  28309  cofcut1  28312  cofcutr  28316  noseqinds  28685  onsfi  28748  elcgrabasrd  29382  cgrabasimass  29384  upgr1elem  29696  subumgredg2  29872  subupgr  29874  upgrreslem  29891  umgrreslem  29892  1hevtxdg1  30093  umgr2v2e  30112  pwrssmgc  33608  tocycfv  33717  cycpm3cl2  33744  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem3  33852  elrgspnlem4  33853  elrgspnsubrunlem1  33855  fldgensdrg  33923  fldgenssv  33924  fldgenssp  33927  nsgmgclem  34009  nsgmgc  34010  nsgqusf1olem2  34012  ssmxidllem  34045  ssmxidl  34046  1arithufdlem1  34123  1arithufdlem2  34124  1arithufdlem3  34125  1arithufdlem4  34126  0mplrim  34193  selvply1rhmlema  34197  selvply1rhmlemb  34198  selvply1rhmlem1  34199  selvply1rhmlem2  34200  selvply1rhmlem4  34202  selvply1rhm0  34205  extvfvvcl  34214  extvfvcl  34215  mplmulmvr  34218  evlextv  34221  mplvrpmlem  34222  mplvrpmfgalem  34223  mplvrpmga  34224  mplvrpmmhm  34225  mplvrpmrhm  34226  psrmonmul  34229  psrmonprod  34231  esplyfval0  34243  esplylem  34245  esplyfv1  34248  esplyfvaln  34253  esplyind  34254  minplymindeg  34387  minplyirredlem  34389  irngnminplynz  34391  irredminply  34395  zarcls1  34548  zarclsiin  34550  zart0  34558  ldgenpisyslem1  34843  fmla1  36239  aks4d1p5  43224  aks4d1p8  43231  primrootsunit1  43241  primrootscoprmpow  43243  primrootscoprbij  43246  hashscontpow1  43265  sticksstones2  43291  grpods  43338  unitscyglem1  43339  unitscyglem2  43340  unitscyglem4  43342  supinf  43387  onintunirab  44323  naddwordnexlem4  44497  supminfrnmpt  46549  supminfxr  46568  supminfxr2  46573  supminfxrrnmpt  46575  sumnnodd  46736  dvnprodlem1  47050  smflimsuplem5  47928  tmachlem-agreeself  48040  lubprlem  50170  intubeu  50192  unilbeu  50193