Theorem elrab2 2962

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 2296	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑})
3		elrab2.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
4	3	elrab 2959	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))
5	2, 4	bitri 184	1 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801

This theorem is referenced by:  elrabsf  3067  pwnss  4242  regexmidlemm  4623  regexmidlem1  4624  reg2exmidlema  4625  tfis  4674  ctssdccl  7274  nninff  7285  nninfninc  7286  infnninf  7287  infnninfOLD  7288  nnnninf  7289  nnnninfeq  7291  nnnninfeq2  7292  nninfwlpoimlemg  7338  exmidaclem  7386  ltexprlemell  7781  ltexprlemelu  7782  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemopu  7831  cauappcvgprlemupu  7832  cauappcvgprlemdisj  7834  cauappcvgprlemloc  7835  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  cauappcvgprlem2  7843  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemopu  7854  caucvgprlemupu  7855  caucvgprlemdisj  7857  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprlem2  7863  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemexbt  7889  caucvgprprlem2  7893  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  axpre-suploclemres  8084  elz  9444  elrp  9847  repos  10162  zsupssdc  10453  bitsfzolem  12460  isprm  12626  oddpwdc  12691  sqpweven  12692  2sqpwodd  12693  phimullem  12742  eulerthlem1  12744  eulerthlemfi  12745  eulerthlemrprm  12746  eulerthlemth  12749  hashgcdlem  12755  pclem0  12804  pclemub  12805  pclemdc  12806  pcprecl  12807  pcprendvds  12808  1arith  12885  elgz  12889  4sqlem13m  12921  4sqlem17  12925  4sqlem18  12926  ctiunctlemu1st  13000  ctiunctlemu2nd  13001  ctiunctlemudc  13003  ctiunctlemfo  13005  infpn2  13022  issgrp  13431  ismnddef  13446  gsumvallem2  13521  isgrp  13534  elnmz  13740  iscmn  13825  isrng  13892  issrg  13923  isring  13958  iscrng  13961  isnzr  14139  islring  14150  isrrg  14221  isdomn  14227  islmod  14249  psrbag  14627  psr1clfi  14646  isxms  15119  isms  15121  ivthinclemlm  15302  ivthinclemum  15303  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemdisj  15308  ivthinclemloc  15309  mpodvdsmulf1o  15658  lgslem2  15674  lgslem3  15675  lgsfcl2  15679  lfgredg2dom  15924  uspgredg2vlem  16012  uspgredg2v  16013  usgredg2vlem1  16014  usgredg2vlem2  16015  ushgredgedg  16018  ushgredgedgloop  16020  0nninf  16329  nnsf  16330  peano4nninf  16331  nninfalllem1  16333  nninfself  16338  qdencn  16354