Theorem elrabd 3647

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {crab 3413

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453

This theorem is used by:  nnawordex  8639  cofon1  8674  ordtypelem7  9511  oemapvali  9678  rankuni2b  9860  harval2  10071  fin23lem11  10388  fin1a2lem11  10481  pinq  11005  negf1o  11739  uzind4  13026  zsupss  13057  flval3  13948  serge0  14192  expge0  14234  expge1  14235  hashbclem  14590  rlimrege0  15739  lcmgcdlem  16774  phicl2  16938  hashdvds  16945  phisum  16961  pcpremul  17014  prmreclem1  17087  prmreclem3  17089  prmreclem5  17091  ramub  17184  ramub1lem1  17197  ramub1lem2  17198  prmgaplem3  17224  prmgaplem4  17225  prmgaplem5  17226  prmgaplem6  17227  mrcflem  17773  mrcval  17777  isacs1i  17824  coaval  18236  gsumress  18864  rabsubmgmd  18886  issubmd  18994  mhmeql  19015  ghmeql  19446  pmtrval  19658  pmtrrn  19664  symgsssg  19674  symgfisg  19675  psgnunilem5  19701  pgpssslw  19821  efgsfo  19946  oddvdssubg  20062  dprdwd  20220  lmhmeql  21323  ssdifidllem  21633  ssdifidl  21634  cofipsgn  21892  frlmssuvc2  22094  gsumbagdiaglem  22232  psrlidm  22262  psrridm  22263  mplmonmul  22338  mhpmulcl  22463  psdmul  22480  coe1fsupp  22525  dmatmulcl  22808  fctop  23315  cctop  23317  ppttop  23318  pptbas  23319  epttop  23320  ordthauslem  23694  cmpsublem  23710  locfincmp  23838  xkoopn  23901  pthaus  23950  txkgen  23964  xkohaus  23965  xkococnlem  23971  nrmr0reg  24061  fbssfi  24149  filssufilg  24223  uffixsn  24237  ufinffr  24241  ufilen  24242  supnfcls  24332  flimfnfcls  24340  alexsubALTlem4  24362  tmdgsum2  24408  symgtgp  24418  ghmcnp  24427  lmle  25615  iundisj  25862  opnmbllem  25915  vitalilem2  25923  aannenlem2  26649  aalioulem2  26653  radcnv0  26736  jensen  27309  ftalem4  27396  ftalem5  27397  efnnfsumcl  27423  efchtdvds  27479  sqff1o  27502  fsumdvdsdiaglem  27503  dvdsppwf1o  27506  dvdsflf1o  27507  muinv  27513  dchrfi  27575  lgsne0  27655  2lgslem1b  27712  cutbdaybnd  28174  madebdaylemlrcut  28278  sltsbday  28296  cofcut1  28299  cofcutr  28303  noseqinds  28672  onsfi  28735  elcgrabasrd  29369  cgrabasimass  29371  upgr1elem  29683  subumgredg2  29859  subupgr  29861  upgrreslem  29878  umgrreslem  29879  1hevtxdg1  30080  umgr2v2e  30099  pwrssmgc  33554  tocycfv  33663  cycpm3cl2  33690  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem3  33798  elrgspnlem4  33799  elrgspnsubrunlem1  33801  fldgensdrg  33869  fldgenssv  33870  fldgenssp  33873  nsgmgclem  33955  nsgmgc  33956  nsgqusf1olem2  33958  ssmxidllem  33991  ssmxidl  33992  1arithufdlem1  34069  1arithufdlem2  34070  1arithufdlem3  34071  1arithufdlem4  34072  0mplrim  34139  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem2  34146  selvply1rhmlem4  34148  selvply1rhm0  34151  extvfvvcl  34160  extvfvcl  34161  mplmulmvr  34164  evlextv  34167  mplvrpmlem  34168  mplvrpmfgalem  34169  mplvrpmga  34170  mplvrpmmhm  34171  mplvrpmrhm  34172  psrmonmul  34175  psrmonprod  34177  esplyfval0  34189  esplylem  34191  esplyfv1  34194  esplyfvaln  34199  esplyind  34200  minplymindeg  34333  minplyirredlem  34335  irngnminplynz  34337  irredminply  34341  zarcls1  34494  zarclsiin  34496  zart0  34504  ldgenpisyslem1  34789  fmla1  36131  aks4d1p5  43110  aks4d1p8  43117  primrootsunit1  43127  primrootscoprmpow  43129  primrootscoprbij  43132  hashscontpow1  43151  sticksstones2  43177  grpods  43224  unitscyglem1  43225  unitscyglem2  43226  unitscyglem4  43228  supinf  43273  fnwe2lem2  44037  fnwe2lem3  44038  onintunirab  44213  naddwordnexlem4  44387  supminfrnmpt  46424  supminfxr  46443  supminfxr2  46448  supminfxrrnmpt  46450  sumnnodd  46611  dvnprodlem1  46925  smflimsuplem5  47803  tmachlem-agreeself  47915  lubprlem  50039  intubeu  50061  unilbeu  50062