Theorem elrabd 3652

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  {crab 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440

This theorem is referenced by:  nnawordex  8562  cofon1  8597  ordtypelem7  9435  oemapvali  9599  rankuni2b  9768  harval2  9912  fin23lem11  10230  fin1a2lem11  10323  pinq  10840  negf1o  11568  uzind4  12825  zsupss  12856  flval3  13737  serge0  13981  expge0  14023  expge1  14024  hashbclem  14377  rlimrege0  15504  lcmgcdlem  16535  phicl2  16697  hashdvds  16704  phisum  16720  pcpremul  16773  prmreclem1  16846  prmreclem3  16848  prmreclem5  16850  ramub  16943  ramub1lem1  16956  ramub1lem2  16957  prmgaplem3  16983  prmgaplem4  16984  prmgaplem5  16985  prmgaplem6  16986  mrcflem  17530  mrcval  17534  isacs1i  17581  coaval  17993  gsumress  18574  rabsubmgmd  18596  issubmd  18698  mhmeql  18718  ghmeql  19136  pmtrval  19348  pmtrrn  19354  symgsssg  19364  symgfisg  19365  psgnunilem5  19391  pgpssslw  19511  efgsfo  19636  oddvdssubg  19752  dprdwd  19910  lmhmeql  20977  cofipsgn  21518  frlmssuvc2  21720  gsumbagdiaglem  21855  psrlidm  21887  psrridm  21888  mplmonmul  21959  mhpmulcl  22052  psdmul  22069  coe1fsupp  22115  dmatmulcl  22403  fctop  22907  cctop  22909  ppttop  22910  pptbas  22911  epttop  22912  ordthauslem  23286  cmpsublem  23302  locfincmp  23429  xkoopn  23492  pthaus  23541  txkgen  23555  xkohaus  23556  xkococnlem  23562  nrmr0reg  23652  fbssfi  23740  filssufilg  23814  uffixsn  23828  ufinffr  23832  ufilen  23833  supnfcls  23923  flimfnfcls  23931  alexsubALTlem4  23953  tmdgsum2  23999  symgtgp  24009  ghmcnp  24018  lmle  25217  iundisj  25465  opnmbllem  25518  vitalilem2  25526  aannenlem2  26253  aalioulem2  26257  radcnv0  26341  jensen  26915  ftalem4  27002  ftalem5  27003  efnnfsumcl  27029  efchtdvds  27085  sqff1o  27108  fsumdvdsdiaglem  27109  dvdsppwf1o  27112  dvdsflf1o  27113  muinv  27119  dchrfi  27182  lgsne0  27262  2lgslem1b  27319  scutbdaybnd  27744  madebdaylemlrcut  27831  cofcut1  27851  cofcutr  27855  noseqinds  28210  onsfi  28270  upgr1elem  29075  subumgredg2  29248  subupgr  29250  upgrreslem  29267  umgrreslem  29268  1hevtxdg1  29470  umgr2v2e  29489  pwrssmgc  32955  tocycfv  33064  cycpm3cl2  33091  elrgspnlem1  33195  elrgspnlem2  33196  elrgspnlem3  33197  elrgspnlem4  33198  elrgspnsubrunlem1  33200  fldgensdrg  33266  fldgenssv  33267  fldgenssp  33270  nsgmgclem  33361  nsgmgc  33362  nsgqusf1olem2  33364  ssdifidllem  33406  ssdifidl  33407  ssmxidllem  33423  ssmxidl  33424  1arithufdlem1  33494  1arithufdlem2  33495  1arithufdlem3  33496  1arithufdlem4  33497  minplymindeg  33677  minplyirredlem  33679  irngnminplynz  33681  irredminply  33685  zarcls1  33838  zarclsiin  33840  zart0  33848  ldgenpisyslem1  34132  fmla1  35362  aks4d1p5  42056  aks4d1p8  42063  primrootsunit1  42073  primrootscoprmpow  42075  primrootscoprbij  42078  hashscontpow1  42097  sticksstones2  42123  grpods  42170  unitscyglem1  42171  unitscyglem2  42172  unitscyglem4  42174  supinf  42218  fnwe2lem2  43027  fnwe2lem3  43028  onintunirab  43203  naddwordnexlem4  43377  supminfrnmpt  45428  supminfxr  45447  supminfxr2  45452  supminfxrrnmpt  45454  dvnprodlem1  45931  smflimsuplem5  46809  lubprlem  48950  intubeu  48972  unilbeu  48973