Theorem elrab2 2966

Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 2-Nov-2006.)

Hypotheses

Ref	Expression
elrab2.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
elrab2.2	⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑}

Assertion

Ref	Expression
elrab2	⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem elrab2

Step	Hyp	Ref	Expression
1		elrab2.2	. . 3 ⊢ 𝐶 = {𝑥 ∈ 𝐵 ∣ 𝜑}
2	1	eleq2i 2298	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 2963	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 184	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2202  {crab 2515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-v 2805

This theorem is referenced by:  elrabsf  3071  pwnss  4255  regexmidlemm  4636  regexmidlem1  4637  reg2exmidlema  4638  tfis  4687  ctssdccl  7353  nninff  7364  nninfninc  7365  infnninf  7366  infnninfOLD  7367  nnnninf  7368  nnnninfeq  7370  nnnninfeq2  7371  nninfwlpoimlemg  7417  exmidaclem  7466  ltexprlemell  7861  ltexprlemelu  7862  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemlol  7910  cauappcvgprlemopu  7911  cauappcvgprlemupu  7912  cauappcvgprlemdisj  7914  cauappcvgprlemloc  7915  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  cauappcvgprlem2  7923  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemopu  7934  caucvgprlemupu  7935  caucvgprlemdisj  7937  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprlem2  7943  caucvgprprlemell  7948  caucvgprprlemelu  7949  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemexbt  7969  caucvgprprlem2  7973  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  axpre-suploclemres  8164  elz  9524  elrp  9933  repos  10248  zsupssdc  10542  bitsfzolem  12576  isprm  12742  oddpwdc  12807  sqpweven  12808  2sqpwodd  12809  phimullem  12858  eulerthlem1  12860  eulerthlemfi  12861  eulerthlemrprm  12862  eulerthlemth  12865  hashgcdlem  12871  pclem0  12920  pclemub  12921  pclemdc  12922  pcprecl  12923  pcprendvds  12924  1arith  13001  elgz  13005  4sqlem13m  13037  4sqlem17  13041  4sqlem18  13042  ctiunctlemu1st  13116  ctiunctlemu2nd  13117  ctiunctlemudc  13119  ctiunctlemfo  13121  infpn2  13138  issgrp  13547  ismnddef  13562  gsumvallem2  13637  isgrp  13650  elnmz  13856  iscmn  13941  isrng  14009  issrg  14040  isring  14075  iscrng  14078  isnzr  14257  islring  14268  isrrg  14339  isdomn  14345  islmod  14367  psrbag  14745  psrbagconcl  14753  psr1clfi  14769  isxms  15242  isms  15244  ivthinclemlm  15425  ivthinclemum  15426  ivthinclemlopn  15427  ivthinclemlr  15428  ivthinclemuopn  15429  ivthinclemur  15430  ivthinclemdisj  15431  ivthinclemloc  15432  mpodvdsmulf1o  15781  lgslem2  15797  lgslem3  15798  lgsfcl2  15802  lfgredg2dom  16050  uspgredg2vlem  16138  uspgredg2v  16139  usgredg2vlem1  16140  usgredg2vlem2  16141  ushgredgedg  16144  ushgredgedgloop  16146  isclwwlknon  16348  s2elclwwlknon2  16354  0nninf  16707  nnsf  16708  peano4nninf  16709  nninfalllem1  16711  nninfself  16716  qdencn  16732