Theorem elrabd 3696

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479

This theorem is referenced by:  nnawordex  8673  cofon1  8708  ordtypelem7  9561  oemapvali  9721  rankuni2b  9890  harval2  10034  fin23lem11  10354  fin1a2lem11  10447  pinq  10964  negf1o  11690  uzind4  12945  zsupss  12976  flval3  13851  serge0  14093  expge0  14135  expge1  14136  hashbclem  14487  rlimrege0  15611  lcmgcdlem  16639  phicl2  16801  hashdvds  16808  phisum  16823  pcpremul  16876  prmreclem1  16949  prmreclem3  16951  prmreclem5  16953  ramub  17046  ramub1lem1  17059  ramub1lem2  17060  prmgaplem3  17086  prmgaplem4  17087  prmgaplem5  17088  prmgaplem6  17089  mrcflem  17650  mrcval  17654  isacs1i  17701  coaval  18121  gsumress  18707  rabsubmgmd  18729  issubmd  18831  mhmeql  18851  ghmeql  19269  pmtrval  19483  pmtrrn  19489  symgsssg  19499  symgfisg  19500  psgnunilem5  19526  pgpssslw  19646  efgsfo  19771  oddvdssubg  19887  dprdwd  20045  lmhmeql  21071  cofipsgn  21628  frlmssuvc2  21832  gsumbagdiaglem  21967  psrlidm  21999  psrridm  22000  mplmonmul  22071  mhpmulcl  22170  psdmul  22187  coe1fsupp  22231  dmatmulcl  22521  fctop  23026  cctop  23028  ppttop  23029  pptbas  23030  epttop  23031  ordthauslem  23406  cmpsublem  23422  locfincmp  23549  xkoopn  23612  pthaus  23661  txkgen  23675  xkohaus  23676  xkococnlem  23682  nrmr0reg  23772  fbssfi  23860  filssufilg  23934  uffixsn  23948  ufinffr  23952  ufilen  23953  supnfcls  24043  flimfnfcls  24051  alexsubALTlem4  24073  tmdgsum2  24119  symgtgp  24129  ghmcnp  24138  lmle  25348  iundisj  25596  opnmbllem  25649  vitalilem2  25657  aannenlem2  26385  aalioulem2  26389  radcnv0  26473  jensen  27046  ftalem4  27133  ftalem5  27134  efnnfsumcl  27160  efchtdvds  27216  sqff1o  27239  fsumdvdsdiaglem  27240  dvdsppwf1o  27243  dvdsflf1o  27244  muinv  27250  dchrfi  27313  lgsne0  27393  2lgslem1b  27450  scutbdaybnd  27874  madebdaylemlrcut  27951  cofcut1  27968  cofcutr  27972  noseqinds  28313  upgr1elem  29143  subumgredg2  29316  subupgr  29318  upgrreslem  29335  umgrreslem  29336  1hevtxdg1  29538  umgr2v2e  29557  pwrssmgc  32974  tocycfv  33111  cycpm3cl2  33138  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  fldgensdrg  33295  fldgenssv  33296  fldgenssp  33299  nsgmgclem  33418  nsgmgc  33419  nsgqusf1olem2  33421  ssdifidllem  33463  ssdifidl  33464  ssmxidllem  33480  ssmxidl  33481  1arithufdlem1  33551  1arithufdlem2  33552  1arithufdlem3  33553  1arithufdlem4  33554  minplymindeg  33715  minplyirredlem  33717  irngnminplynz  33719  irredminply  33721  zarcls1  33829  zarclsiin  33831  zart0  33839  ldgenpisyslem1  34143  fmla1  35371  aks4d1p5  42061  aks4d1p8  42068  primrootsunit1  42078  primrootscoprmpow  42080  primrootscoprbij  42083  hashscontpow1  42102  sticksstones2  42128  grpods  42175  unitscyglem1  42176  unitscyglem2  42177  unitscyglem4  42179  supinf  42261  fnwe2lem2  43039  fnwe2lem3  43040  onintunirab  43215  naddwordnexlem4  43390  supminfrnmpt  45394  supminfxr  45413  supminfxr2  45418  supminfxrrnmpt  45420  dvnprodlem1  45901  smflimsuplem5  46779  lubprlem  48758  intubeu  48772  unilbeu  48773