Theorem elrabd 3637

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3390

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432

This theorem is referenced by:  nnawordex  8566  cofon1  8601  ordtypelem7  9432  oemapvali  9596  rankuni2b  9768  harval2  9912  fin23lem11  10230  fin1a2lem11  10323  pinq  10841  negf1o  11571  uzind4  12847  zsupss  12878  flval3  13765  serge0  14009  expge0  14051  expge1  14052  hashbclem  14405  rlimrege0  15532  lcmgcdlem  16566  phicl2  16729  hashdvds  16736  phisum  16752  pcpremul  16805  prmreclem1  16878  prmreclem3  16880  prmreclem5  16882  ramub  16975  ramub1lem1  16988  ramub1lem2  16989  prmgaplem3  17015  prmgaplem4  17016  prmgaplem5  17017  prmgaplem6  17018  mrcflem  17563  mrcval  17567  isacs1i  17614  coaval  18026  gsumress  18641  rabsubmgmd  18663  issubmd  18765  mhmeql  18785  ghmeql  19205  pmtrval  19417  pmtrrn  19423  symgsssg  19433  symgfisg  19434  psgnunilem5  19460  pgpssslw  19580  efgsfo  19705  oddvdssubg  19821  dprdwd  19979  lmhmeql  21042  cofipsgn  21583  frlmssuvc2  21785  gsumbagdiaglem  21920  psrlidm  21950  psrridm  21951  mplmonmul  22024  mhpmulcl  22125  psdmul  22142  coe1fsupp  22188  dmatmulcl  22475  fctop  22979  cctop  22981  ppttop  22982  pptbas  22983  epttop  22984  ordthauslem  23358  cmpsublem  23374  locfincmp  23501  xkoopn  23564  pthaus  23613  txkgen  23627  xkohaus  23628  xkococnlem  23634  nrmr0reg  23724  fbssfi  23812  filssufilg  23886  uffixsn  23900  ufinffr  23904  ufilen  23905  supnfcls  23995  flimfnfcls  24003  alexsubALTlem4  24025  tmdgsum2  24071  symgtgp  24081  ghmcnp  24090  lmle  25278  iundisj  25525  opnmbllem  25578  vitalilem2  25586  aannenlem2  26306  aalioulem2  26310  radcnv0  26394  jensen  26966  ftalem4  27053  ftalem5  27054  efnnfsumcl  27080  efchtdvds  27136  sqff1o  27159  fsumdvdsdiaglem  27160  dvdsppwf1o  27163  dvdsflf1o  27164  muinv  27170  dchrfi  27232  lgsne0  27312  2lgslem1b  27369  cutbdaybnd  27801  madebdaylemlrcut  27905  sltsbday  27923  cofcut1  27926  cofcutr  27930  noseqinds  28299  onsfi  28362  upgr1elem  29195  subumgredg2  29368  subupgr  29370  upgrreslem  29387  umgrreslem  29388  1hevtxdg1  29590  umgr2v2e  29609  pwrssmgc  33075  tocycfv  33185  cycpm3cl2  33212  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspnsubrunlem1  33323  fldgensdrg  33390  fldgenssv  33391  fldgenssp  33394  nsgmgclem  33486  nsgmgc  33487  nsgqusf1olem2  33489  ssdifidllem  33531  ssdifidl  33532  ssmxidllem  33548  ssmxidl  33549  1arithufdlem1  33619  1arithufdlem2  33620  1arithufdlem3  33621  1arithufdlem4  33622  extvfvvcl  33694  extvfvcl  33695  mplmulmvr  33698  evlextv  33701  mplvrpmlem  33702  mplvrpmfgalem  33703  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  psrmonmul  33709  psrmonprod  33711  esplyfval0  33723  esplylem  33725  esplyfv1  33728  esplyfvaln  33733  esplyind  33734  minplymindeg  33868  minplyirredlem  33870  irngnminplynz  33872  irredminply  33876  zarcls1  34029  zarclsiin  34031  zart0  34039  ldgenpisyslem1  34323  fmla1  35585  aks4d1p5  42533  aks4d1p8  42540  primrootsunit1  42550  primrootscoprmpow  42552  primrootscoprbij  42555  hashscontpow1  42574  sticksstones2  42600  grpods  42647  unitscyglem1  42648  unitscyglem2  42649  unitscyglem4  42651  supinf  42695  fnwe2lem2  43497  fnwe2lem3  43498  onintunirab  43673  naddwordnexlem4  43847  supminfrnmpt  45891  supminfxr  45910  supminfxr2  45915  supminfxrrnmpt  45917  dvnprodlem1  46392  smflimsuplem5  47270  lubprlem  49449  intubeu  49471  unilbeu  49472