Theorem elrabd 3593

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543   ∈ wcel 2112  {crab 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400

This theorem is referenced by:  nnawordex  8343  ordtypelem7  9118  oemapvali  9277  rankuni2b  9434  harval2  9578  fin23lem11  9896  fin1a2lem11  9989  pinq  10506  negf1o  11227  uzind4  12467  zsupss  12498  flval3  13355  serge0  13595  expge0  13636  expge1  13637  hashbclem  13981  rlimrege0  15105  lcmgcdlem  16126  phicl2  16284  hashdvds  16291  phisum  16306  pcpremul  16359  prmreclem1  16432  prmreclem3  16434  prmreclem5  16436  ramub  16529  ramub1lem1  16542  ramub1lem2  16543  prmgaplem3  16569  prmgaplem4  16570  prmgaplem5  16571  prmgaplem6  16572  mrcflem  17063  mrcval  17067  isacs1i  17114  coaval  17528  gsumress  18108  issubmd  18187  mhmeql  18206  ghmeql  18599  pmtrval  18797  pmtrrn  18803  symgsssg  18813  symgfisg  18814  psgnunilem5  18840  pgpssslw  18957  efgsfo  19083  oddvdssubg  19194  dprdwd  19352  lmhmeql  20046  cofipsgn  20509  frlmssuvc2  20711  gsumbagdiaglemOLD  20851  gsumbagdiaglem  20854  psrlidm  20882  psrridm  20883  mplmonmul  20947  mhpmulcl  21043  coe1fsupp  21089  dmatmulcl  21351  fctop  21855  cctop  21857  ppttop  21858  pptbas  21859  epttop  21860  ordthauslem  22234  cmpsublem  22250  locfincmp  22377  xkoopn  22440  pthaus  22489  txkgen  22503  xkohaus  22504  xkococnlem  22510  nrmr0reg  22600  fbssfi  22688  filssufilg  22762  uffixsn  22776  ufinffr  22780  ufilen  22781  supnfcls  22871  flimfnfcls  22879  alexsubALTlem4  22901  tmdgsum2  22947  symgtgp  22957  ghmcnp  22966  lmle  24152  iundisj  24399  opnmbllem  24452  vitalilem2  24460  aannenlem2  25176  aalioulem2  25180  radcnv0  25262  jensen  25825  ftalem4  25912  ftalem5  25913  efnnfsumcl  25939  efchtdvds  25995  sqff1o  26018  fsumdvdsdiaglem  26019  dvdsppwf1o  26022  dvdsflf1o  26023  muinv  26029  dchrfi  26090  lgsne0  26170  2lgslem1b  26227  upgr1elem  27157  subumgredg2  27327  subupgr  27329  upgrreslem  27346  umgrreslem  27347  1hevtxdg1  27548  umgr2v2e  27567  pwrssmgc  30951  tocycfv  31049  cycpm3cl2  31076  nsgmgclem  31264  nsgmgc  31265  nsgqusf1olem2  31267  ssmxidllem  31309  ssmxidl  31310  zarcls1  31487  zarclsiin  31489  zart0  31497  ldgenpisyslem1  31797  fmla1  33016  scutbdaybnd  33695  madebdaylemlrcut  33765  cofcut1  33776  cofcutr  33778  sticksstones2  39772  fnwe2lem2  40520  fnwe2lem3  40521  supminfrnmpt  42599  supminfxr  42620  supminfxr2  42625  supminfxrrnmpt  42627  smflimsuplem5  43972  rabsubmgmd  44961  lubprlem  45872  intubeu  45886  unilbeu  45887