Theorem elrabd 3592

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ∈ wcel 2048  {crab 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411

This theorem is referenced by:  nnawordex  8056  ordtypelem7  8775  oemapvali  8933  rankuni2b  9068  harval2  9212  fin23lem11  9529  fin1a2lem11  9622  pinq  10139  negf1o  10863  fiminreOLD  11383  uzind4  12113  zsupss  12144  flval3  12993  serge0  13232  expge0  13273  expge1  13274  hashbclem  13613  rlimrege0  14787  lcmgcdlem  15796  phicl2  15951  hashdvds  15958  phisum  15973  pcpremul  16026  prmreclem1  16098  prmreclem3  16100  prmreclem5  16102  ramub  16195  ramub1lem1  16208  ramub1lem2  16209  prmgaplem3  16235  prmgaplem4  16236  prmgaplem5  16237  prmgaplem6  16238  mrcflem  16725  mrcval  16729  isacs1i  16776  coaval  17176  gsumress  17734  issubmd  17807  mhmeql  17822  ghmeql  18142  pmtrval  18330  pmtrrn  18336  symgsssg  18346  symgfisg  18347  psgnunilem5  18373  pgpssslw  18490  efgsfo  18614  oddvdssubg  18721  dprdwd  18873  lmhmeql  19539  gsumbagdiaglem  19859  psrlidm  19887  psrridm  19888  mplmonmul  19948  coe1fsupp  20075  cofipsgn  20429  frlmssuvc2  20631  dmatmulcl  20803  fctop  21306  cctop  21308  ppttop  21309  pptbas  21310  epttop  21311  ordthauslem  21685  cmpsublem  21701  locfincmp  21828  xkoopn  21891  pthaus  21940  txkgen  21954  xkohaus  21955  xkococnlem  21961  nrmr0reg  22051  fbssfi  22139  filssufilg  22213  uffixsn  22227  ufinffr  22231  ufilen  22232  supnfcls  22322  flimfnfcls  22330  alexsubALTlem4  22352  tmdgsum2  22398  symgtgp  22403  ghmcnp  22416  lmle  23597  iundisj  23842  opnmbllem  23895  vitalilem2  23903  aannenlem2  24611  aalioulem2  24615  radcnv0  24697  jensen  25258  ftalem4  25345  ftalem5  25346  efnnfsumcl  25372  efchtdvds  25428  sqff1o  25451  fsumdvdsdiaglem  25452  dvdsppwf1o  25455  dvdsflf1o  25456  muinv  25462  dchrfi  25523  lgsne0  25603  2lgslem1b  25660  upgr1elem  26590  subumgredg2  26760  subupgr  26762  upgrreslem  26779  umgrreslem  26780  1hevtxdg1  26981  umgr2v2e  27000  fnwe2lem2  38992  fnwe2lem3  38993  supminfrnmpt  41096  supminfxr  41117  supminfxr2  41122  supminfxrrnmpt  41124  smflimsuplem5  42475  rabsubmgmd  43366