Theorem elrabd 3653

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2143  {crab 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457

This theorem is referenced by:  nnawordex  8624  cofon1  8659  ordtypelem7  9487  oemapvali  9654  rankuni2b  9826  harval2  9984  fin23lem11  10302  fin1a2lem11  10395  pinq  10913  negf1o  11645  uzind4  12931  zsupss  12962  flval3  13850  serge0  14094  expge0  14136  expge1  14137  hashbclem  14491  rlimrege0  15632  lcmgcdlem  16665  phicl2  16828  hashdvds  16835  phisum  16851  pcpremul  16904  prmreclem1  16977  prmreclem3  16979  prmreclem5  16981  ramub  17074  ramub1lem1  17087  ramub1lem2  17088  prmgaplem3  17114  prmgaplem4  17115  prmgaplem5  17116  prmgaplem6  17117  mrcflem  17663  mrcval  17667  isacs1i  17714  coaval  18126  gsumress  18741  rabsubmgmd  18763  issubmd  18865  mhmeql  18886  ghmeql  19310  pmtrval  19522  pmtrrn  19528  symgsssg  19538  symgfisg  19539  psgnunilem5  19565  pgpssslw  19685  efgsfo  19810  oddvdssubg  19926  dprdwd  20084  lmhmeql  21157  ssdifidllem  21465  ssdifidl  21466  cofipsgn  21724  frlmssuvc2  21926  gsumbagdiaglem  22062  psrlidm  22092  psrridm  22093  mplmonmul  22168  mhpmulcl  22293  psdmul  22310  coe1fsupp  22355  dmatmulcl  22638  fctop  23142  cctop  23144  ppttop  23145  pptbas  23146  epttop  23147  ordthauslem  23521  cmpsublem  23537  locfincmp  23664  xkoopn  23727  pthaus  23776  txkgen  23790  xkohaus  23791  xkococnlem  23797  nrmr0reg  23887  fbssfi  23975  filssufilg  24049  uffixsn  24063  ufinffr  24067  ufilen  24068  supnfcls  24158  flimfnfcls  24166  alexsubALTlem4  24188  tmdgsum2  24234  symgtgp  24244  ghmcnp  24253  lmle  25441  iundisj  25688  opnmbllem  25741  vitalilem2  25749  aannenlem2  26473  aalioulem2  26477  radcnv0  26560  jensen  27134  ftalem4  27221  ftalem5  27222  efnnfsumcl  27248  efchtdvds  27304  sqff1o  27327  fsumdvdsdiaglem  27328  dvdsppwf1o  27331  dvdsflf1o  27332  muinv  27338  dchrfi  27400  lgsne0  27480  2lgslem1b  27537  cutbdaybnd  27969  madebdaylemlrcut  28073  sltsbday  28091  cofcut1  28094  cofcutr  28098  noseqinds  28467  onsfi  28530  upgr1elem  29443  subumgredg2  29616  subupgr  29618  upgrreslem  29635  umgrreslem  29636  1hevtxdg1  29837  umgr2v2e  29856  pwrssmgc  33301  tocycfv  33410  cycpm3cl2  33437  elrgspnlem1  33543  elrgspnlem2  33544  elrgspnlem3  33545  elrgspnlem4  33546  elrgspnsubrunlem1  33548  fldgensdrg  33616  fldgenssv  33617  fldgenssp  33620  nsgmgclem  33701  nsgmgc  33702  nsgqusf1olem2  33704  ssmxidllem  33737  ssmxidl  33738  1arithufdlem1  33815  1arithufdlem2  33816  1arithufdlem3  33817  1arithufdlem4  33818  0mplrim  33885  selvply1rhmlema  33889  selvply1rhmlemb  33890  selvply1rhmlem1  33891  selvply1rhmlem2  33892  selvply1rhmlem4  33894  selvply1rhm0  33897  extvfvvcl  33906  extvfvcl  33907  mplmulmvr  33910  evlextv  33913  mplvrpmlem  33914  mplvrpmfgalem  33915  mplvrpmga  33916  mplvrpmmhm  33917  mplvrpmrhm  33918  psrmonmul  33921  psrmonprod  33923  esplyfval0  33935  esplylem  33937  esplyfv1  33940  esplyfvaln  33945  esplyind  33946  minplymindeg  34079  minplyirredlem  34081  irngnminplynz  34083  irredminply  34087  zarcls1  34240  zarclsiin  34242  zart0  34250  ldgenpisyslem1  34534  fmla1  35860  aks4d1p5  42828  aks4d1p8  42835  primrootsunit1  42845  primrootscoprmpow  42847  primrootscoprbij  42850  hashscontpow1  42869  sticksstones2  42895  grpods  42942  unitscyglem1  42943  unitscyglem2  42944  unitscyglem4  42946  supinf  42991  fnwe2lem2  43761  fnwe2lem3  43762  onintunirab  43937  naddwordnexlem4  44111  supminfrnmpt  46142  supminfxr  46161  supminfxr2  46166  supminfxrrnmpt  46168  dvnprodlem1  46643  smflimsuplem5  47521  lubprlem  49723  intubeu  49745  unilbeu  49746