Theorem elrabd 3636

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431

This theorem is referenced by:  nnawordex  8573  cofon1  8608  ordtypelem7  9439  oemapvali  9605  rankuni2b  9777  harval2  9921  fin23lem11  10239  fin1a2lem11  10332  pinq  10850  negf1o  11580  uzind4  12856  zsupss  12887  flval3  13774  serge0  14018  expge0  14060  expge1  14061  hashbclem  14414  rlimrege0  15541  lcmgcdlem  16575  phicl2  16738  hashdvds  16745  phisum  16761  pcpremul  16814  prmreclem1  16887  prmreclem3  16889  prmreclem5  16891  ramub  16984  ramub1lem1  16997  ramub1lem2  16998  prmgaplem3  17024  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  mrcflem  17572  mrcval  17576  isacs1i  17623  coaval  18035  gsumress  18650  rabsubmgmd  18672  issubmd  18774  mhmeql  18794  ghmeql  19214  pmtrval  19426  pmtrrn  19432  symgsssg  19442  symgfisg  19443  psgnunilem5  19469  pgpssslw  19589  efgsfo  19714  oddvdssubg  19830  dprdwd  19988  lmhmeql  21050  cofipsgn  21573  frlmssuvc2  21775  gsumbagdiaglem  21910  psrlidm  21940  psrridm  21941  mplmonmul  22014  mhpmulcl  22115  psdmul  22132  coe1fsupp  22178  dmatmulcl  22465  fctop  22969  cctop  22971  ppttop  22972  pptbas  22973  epttop  22974  ordthauslem  23348  cmpsublem  23364  locfincmp  23491  xkoopn  23554  pthaus  23603  txkgen  23617  xkohaus  23618  xkococnlem  23624  nrmr0reg  23714  fbssfi  23802  filssufilg  23876  uffixsn  23890  ufinffr  23894  ufilen  23895  supnfcls  23985  flimfnfcls  23993  alexsubALTlem4  24015  tmdgsum2  24061  symgtgp  24071  ghmcnp  24080  lmle  25268  iundisj  25515  opnmbllem  25568  vitalilem2  25576  aannenlem2  26295  aalioulem2  26299  radcnv0  26381  jensen  26952  ftalem4  27039  ftalem5  27040  efnnfsumcl  27066  efchtdvds  27122  sqff1o  27145  fsumdvdsdiaglem  27146  dvdsppwf1o  27149  dvdsflf1o  27150  muinv  27156  dchrfi  27218  lgsne0  27298  2lgslem1b  27355  cutbdaybnd  27787  madebdaylemlrcut  27891  sltsbday  27909  cofcut1  27912  cofcutr  27916  noseqinds  28285  onsfi  28348  upgr1elem  29181  subumgredg2  29354  subupgr  29356  upgrreslem  29373  umgrreslem  29374  1hevtxdg1  29575  umgr2v2e  29594  pwrssmgc  33060  tocycfv  33170  cycpm3cl2  33197  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspnsubrunlem1  33308  fldgensdrg  33375  fldgenssv  33376  fldgenssp  33379  nsgmgclem  33471  nsgmgc  33472  nsgqusf1olem2  33474  ssdifidllem  33516  ssdifidl  33517  ssmxidllem  33533  ssmxidl  33534  1arithufdlem1  33604  1arithufdlem2  33605  1arithufdlem3  33606  1arithufdlem4  33607  extvfvvcl  33679  extvfvcl  33680  mplmulmvr  33683  evlextv  33686  mplvrpmlem  33687  mplvrpmfgalem  33688  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonmul  33694  psrmonprod  33696  esplyfval0  33708  esplylem  33710  esplyfv1  33713  esplyfvaln  33718  esplyind  33719  minplymindeg  33852  minplyirredlem  33854  irngnminplynz  33856  irredminply  33860  zarcls1  34013  zarclsiin  34015  zart0  34023  ldgenpisyslem1  34307  fmla1  35569  aks4d1p5  42519  aks4d1p8  42526  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  hashscontpow1  42560  sticksstones2  42586  grpods  42633  unitscyglem1  42634  unitscyglem2  42635  unitscyglem4  42637  supinf  42681  fnwe2lem2  43479  fnwe2lem3  43480  onintunirab  43655  naddwordnexlem4  43829  supminfrnmpt  45873  supminfxr  45892  supminfxr2  45897  supminfxrrnmpt  45899  dvnprodlem1  46374  smflimsuplem5  47252  lubprlem  49437  intubeu  49459  unilbeu  49460