Theorem elrabd 3648

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442

This theorem is referenced by:  nnawordex  8565  cofon1  8600  ordtypelem7  9429  oemapvali  9593  rankuni2b  9765  harval2  9909  fin23lem11  10227  fin1a2lem11  10320  pinq  10838  negf1o  11567  uzind4  12819  zsupss  12850  flval3  13735  serge0  13979  expge0  14021  expge1  14022  hashbclem  14375  rlimrege0  15502  lcmgcdlem  16533  phicl2  16695  hashdvds  16702  phisum  16718  pcpremul  16771  prmreclem1  16844  prmreclem3  16846  prmreclem5  16848  ramub  16941  ramub1lem1  16954  ramub1lem2  16955  prmgaplem3  16981  prmgaplem4  16982  prmgaplem5  16983  prmgaplem6  16984  mrcflem  17529  mrcval  17533  isacs1i  17580  coaval  17992  gsumress  18607  rabsubmgmd  18629  issubmd  18731  mhmeql  18751  ghmeql  19168  pmtrval  19380  pmtrrn  19386  symgsssg  19396  symgfisg  19397  psgnunilem5  19423  pgpssslw  19543  efgsfo  19668  oddvdssubg  19784  dprdwd  19942  lmhmeql  21007  cofipsgn  21548  frlmssuvc2  21750  gsumbagdiaglem  21886  psrlidm  21917  psrridm  21918  mplmonmul  21991  mhpmulcl  22092  psdmul  22109  coe1fsupp  22155  dmatmulcl  22444  fctop  22948  cctop  22950  ppttop  22951  pptbas  22952  epttop  22953  ordthauslem  23327  cmpsublem  23343  locfincmp  23470  xkoopn  23533  pthaus  23582  txkgen  23596  xkohaus  23597  xkococnlem  23603  nrmr0reg  23693  fbssfi  23781  filssufilg  23855  uffixsn  23869  ufinffr  23873  ufilen  23874  supnfcls  23964  flimfnfcls  23972  alexsubALTlem4  23994  tmdgsum2  24040  symgtgp  24050  ghmcnp  24059  lmle  25257  iundisj  25505  opnmbllem  25558  vitalilem2  25566  aannenlem2  26293  aalioulem2  26297  radcnv0  26381  jensen  26955  ftalem4  27042  ftalem5  27043  efnnfsumcl  27069  efchtdvds  27125  sqff1o  27148  fsumdvdsdiaglem  27149  dvdsppwf1o  27152  dvdsflf1o  27153  muinv  27159  dchrfi  27222  lgsne0  27302  2lgslem1b  27359  cutbdaybnd  27791  madebdaylemlrcut  27895  sltsbday  27913  cofcut1  27916  cofcutr  27920  noseqinds  28289  onsfi  28352  upgr1elem  29185  subumgredg2  29358  subupgr  29360  upgrreslem  29377  umgrreslem  29378  1hevtxdg1  29580  umgr2v2e  29599  pwrssmgc  33082  tocycfv  33191  cycpm3cl2  33218  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspnsubrunlem1  33329  fldgensdrg  33396  fldgenssv  33397  fldgenssp  33400  nsgmgclem  33492  nsgmgc  33493  nsgqusf1olem2  33495  ssdifidllem  33537  ssdifidl  33538  ssmxidllem  33554  ssmxidl  33555  1arithufdlem1  33625  1arithufdlem2  33626  1arithufdlem3  33627  1arithufdlem4  33628  extvfvvcl  33700  extvfvcl  33701  mplmulmvr  33704  evlextv  33707  mplvrpmlem  33708  mplvrpmfgalem  33709  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  esplyfval0  33722  esplylem  33724  esplyfv1  33727  esplyind  33731  minplymindeg  33865  minplyirredlem  33867  irngnminplynz  33869  irredminply  33873  zarcls1  34026  zarclsiin  34028  zart0  34036  ldgenpisyslem1  34320  fmla1  35581  aks4d1p5  42334  aks4d1p8  42341  primrootsunit1  42351  primrootscoprmpow  42353  primrootscoprbij  42356  hashscontpow1  42375  sticksstones2  42401  grpods  42448  unitscyglem1  42449  unitscyglem2  42450  unitscyglem4  42452  supinf  42497  fnwe2lem2  43293  fnwe2lem3  43294  onintunirab  43469  naddwordnexlem4  43643  supminfrnmpt  45689  supminfxr  45708  supminfxr2  45713  supminfxrrnmpt  45715  dvnprodlem1  46190  smflimsuplem5  47068  lubprlem  49207  intubeu  49229  unilbeu  49230