Theorem elrabd 3631

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ∈ wcel 2119  {crab 3391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433

This theorem is referenced by:  nnawordex  8563  cofon1  8598  ordtypelem7  9429  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  21045  cofipsgn  21568  frlmssuvc2  21770  gsumbagdiaglem  21906  psrlidm  21936  psrridm  21937  mplmonmul  22012  mhpmulcl  22137  psdmul  22154  coe1fsupp  22199  dmatmulcl  22483  fctop  22987  cctop  22989  ppttop  22990  pptbas  22991  epttop  22992  ordthauslem  23366  cmpsublem  23382  locfincmp  23509  xkoopn  23572  pthaus  23621  txkgen  23635  xkohaus  23636  xkococnlem  23642  nrmr0reg  23732  fbssfi  23820  filssufilg  23894  uffixsn  23908  ufinffr  23912  ufilen  23913  supnfcls  24003  flimfnfcls  24011  alexsubALTlem4  24033  tmdgsum2  24079  symgtgp  24089  ghmcnp  24098  lmle  25286  iundisj  25533  opnmbllem  25586  vitalilem2  25594  aannenlem2  26313  aalioulem2  26317  radcnv0  26399  jensen  26970  ftalem4  27057  ftalem5  27058  efnnfsumcl  27084  efchtdvds  27140  sqff1o  27163  fsumdvdsdiaglem  27164  dvdsppwf1o  27167  dvdsflf1o  27168  muinv  27174  dchrfi  27236  lgsne0  27316  2lgslem1b  27373  cutbdaybnd  27805  madebdaylemlrcut  27909  sltsbday  27927  cofcut1  27930  cofcutr  27934  noseqinds  28303  onsfi  28366  upgr1elem  29199  subumgredg2  29372  subupgr  29374  upgrreslem  29391  umgrreslem  29392  1hevtxdg1  29593  umgr2v2e  29612  pwrssmgc  33079  tocycfv  33190  cycpm3cl2  33217  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem3  33325  elrgspnlem4  33326  elrgspnsubrunlem1  33328  fldgensdrg  33398  fldgenssv  33399  fldgenssp  33402  nsgmgclem  33494  nsgmgc  33495  nsgqusf1olem2  33497  ssdifidllem  33539  ssdifidl  33540  ssmxidllem  33556  ssmxidl  33557  1arithufdlem1  33627  1arithufdlem2  33628  1arithufdlem3  33629  1arithufdlem4  33630  0mplrim  33698  selvply1rhmlema  33702  selvply1rhmlemb  33703  selvply1rhmlem1  33704  selvply1rhmlem2  33705  selvply1rhmlem4  33707  selvply1rhm0  33710  extvfvvcl  33719  extvfvcl  33720  mplmulmvr  33723  evlextv  33726  mplvrpmlem  33727  mplvrpmfgalem  33728  mplvrpmga  33729  mplvrpmmhm  33730  mplvrpmrhm  33731  psrmonmul  33734  psrmonprod  33736  esplyfval0  33748  esplylem  33750  esplyfv1  33753  esplyfvaln  33758  esplyind  33759  minplymindeg  33892  minplyirredlem  33894  irngnminplynz  33896  irredminply  33900  zarcls1  34053  zarclsiin  34055  zart0  34063  ldgenpisyslem1  34347  fmla1  35615  aks4d1p5  42565  aks4d1p8  42572  primrootsunit1  42582  primrootscoprmpow  42584  primrootscoprbij  42587  hashscontpow1  42606  sticksstones2  42632  grpods  42679  unitscyglem1  42680  unitscyglem2  42681  unitscyglem4  42683  supinf  42726  fnwe2lem2  43496  fnwe2lem3  43497  onintunirab  43672  naddwordnexlem4  43846  supminfrnmpt  45888  supminfxr  45907  supminfxr2  45912  supminfxrrnmpt  45914  dvnprodlem1  46389  smflimsuplem5  47267  lubprlem  49452  intubeu  49474  unilbeu  49475