Theorem elrabd 3664

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452

This theorem is referenced by:  nnawordex  8604  cofon1  8639  ordtypelem7  9484  oemapvali  9644  rankuni2b  9813  harval2  9957  fin23lem11  10277  fin1a2lem11  10370  pinq  10887  negf1o  11615  uzind4  12872  zsupss  12903  flval3  13784  serge0  14028  expge0  14070  expge1  14071  hashbclem  14424  rlimrege0  15552  lcmgcdlem  16583  phicl2  16745  hashdvds  16752  phisum  16768  pcpremul  16821  prmreclem1  16894  prmreclem3  16896  prmreclem5  16898  ramub  16991  ramub1lem1  17004  ramub1lem2  17005  prmgaplem3  17031  prmgaplem4  17032  prmgaplem5  17033  prmgaplem6  17034  mrcflem  17574  mrcval  17578  isacs1i  17625  coaval  18037  gsumress  18616  rabsubmgmd  18638  issubmd  18740  mhmeql  18760  ghmeql  19178  pmtrval  19388  pmtrrn  19394  symgsssg  19404  symgfisg  19405  psgnunilem5  19431  pgpssslw  19551  efgsfo  19676  oddvdssubg  19792  dprdwd  19950  lmhmeql  20969  cofipsgn  21509  frlmssuvc2  21711  gsumbagdiaglem  21846  psrlidm  21878  psrridm  21879  mplmonmul  21950  mhpmulcl  22043  psdmul  22060  coe1fsupp  22106  dmatmulcl  22394  fctop  22898  cctop  22900  ppttop  22901  pptbas  22902  epttop  22903  ordthauslem  23277  cmpsublem  23293  locfincmp  23420  xkoopn  23483  pthaus  23532  txkgen  23546  xkohaus  23547  xkococnlem  23553  nrmr0reg  23643  fbssfi  23731  filssufilg  23805  uffixsn  23819  ufinffr  23823  ufilen  23824  supnfcls  23914  flimfnfcls  23922  alexsubALTlem4  23944  tmdgsum2  23990  symgtgp  24000  ghmcnp  24009  lmle  25208  iundisj  25456  opnmbllem  25509  vitalilem2  25517  aannenlem2  26244  aalioulem2  26248  radcnv0  26332  jensen  26906  ftalem4  26993  ftalem5  26994  efnnfsumcl  27020  efchtdvds  27076  sqff1o  27099  fsumdvdsdiaglem  27100  dvdsppwf1o  27103  dvdsflf1o  27104  muinv  27110  dchrfi  27173  lgsne0  27253  2lgslem1b  27310  scutbdaybnd  27734  madebdaylemlrcut  27817  cofcut1  27835  cofcutr  27839  noseqinds  28194  onsfi  28254  upgr1elem  29046  subumgredg2  29219  subupgr  29221  upgrreslem  29238  umgrreslem  29239  1hevtxdg1  29441  umgr2v2e  29460  pwrssmgc  32933  tocycfv  33073  cycpm3cl2  33100  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspnsubrunlem1  33205  fldgensdrg  33271  fldgenssv  33272  fldgenssp  33275  nsgmgclem  33389  nsgmgc  33390  nsgqusf1olem2  33392  ssdifidllem  33434  ssdifidl  33435  ssmxidllem  33451  ssmxidl  33452  1arithufdlem1  33522  1arithufdlem2  33523  1arithufdlem3  33524  1arithufdlem4  33525  minplymindeg  33705  minplyirredlem  33707  irngnminplynz  33709  irredminply  33713  zarcls1  33866  zarclsiin  33868  zart0  33876  ldgenpisyslem1  34160  fmla1  35381  aks4d1p5  42075  aks4d1p8  42082  primrootsunit1  42092  primrootscoprmpow  42094  primrootscoprbij  42097  hashscontpow1  42116  sticksstones2  42142  grpods  42189  unitscyglem1  42190  unitscyglem2  42191  unitscyglem4  42193  supinf  42237  fnwe2lem2  43047  fnwe2lem3  43048  onintunirab  43223  naddwordnexlem4  43397  supminfrnmpt  45448  supminfxr  45467  supminfxr2  45472  supminfxrrnmpt  45474  dvnprodlem1  45951  smflimsuplem5  46829  lubprlem  48954  intubeu  48976  unilbeu  48977