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  9525  elrp  9934  repos  10249  zsupssdc  10544  bitsfzolem  12578  isprm  12744  oddpwdc  12809  sqpweven  12810  2sqpwodd  12811  phimullem  12860  eulerthlem1  12862  eulerthlemfi  12863  eulerthlemrprm  12864  eulerthlemth  12867  hashgcdlem  12873  pclem0  12922  pclemub  12923  pclemdc  12924  pcprecl  12925  pcprendvds  12926  1arith  13003  elgz  13007  4sqlem13m  13039  4sqlem17  13043  4sqlem18  13044  ctiunctlemu1st  13118  ctiunctlemu2nd  13119  ctiunctlemudc  13121  ctiunctlemfo  13123  infpn2  13140  issgrp  13549  ismnddef  13564  gsumvallem2  13639  isgrp  13652  elnmz  13858  iscmn  13943  isrng  14011  issrg  14042  isring  14077  iscrng  14080  isnzr  14259  islring  14270  isrrg  14341  isdomn  14348  islmod  14370  psrbag  14748  psrbagconcl  14756  psr1clfi  14772  isxms  15245  isms  15247  ivthinclemlm  15428  ivthinclemum  15429  ivthinclemlopn  15430  ivthinclemlr  15431  ivthinclemuopn  15432  ivthinclemur  15433  ivthinclemdisj  15434  ivthinclemloc  15435  mpodvdsmulf1o  15787  lgslem2  15803  lgslem3  15804  lgsfcl2  15808  lfgredg2dom  16056  uspgredg2vlem  16144  uspgredg2v  16145  usgredg2vlem1  16146  usgredg2vlem2  16147  ushgredgedg  16150  ushgredgedgloop  16152  isclwwlknon  16354  s2elclwwlknon2  16360  0nninf  16713  nnsf  16714  peano4nninf  16715  nninfalllem1  16717  nninfself  16722  qdencn  16738