Theorem elrab2 2985

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {crab 2532

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is referenced by:  elrabsf  3090  pwnss  4291  regexmidlemm  4674  regexmidlem1  4675  reg2exmidlema  4676  tfis  4725  ctssdccl  7441  nninff  7452  nninfninc  7453  infnninf  7454  infnninfOLD  7455  nnnninf  7456  nnnninfeq  7458  nnnninfeq2  7459  nninfwlpoimlemg  7505  exmidaclem  7554  ltexprlemell  7955  ltexprlemelu  7956  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemlol  8004  cauappcvgprlemopu  8005  cauappcvgprlemupu  8006  cauappcvgprlemdisj  8008  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  cauappcvgprlem2  8017  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemopu  8028  caucvgprlemupu  8029  caucvgprlemdisj  8031  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlem2  8037  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemexbt  8063  caucvgprprlem2  8067  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  axpre-suploclemres  8258  elz  9625  elrp  10035  repos  10351  zsupssdc  10651  bitsfzolem  12699  isprm  12865  oddpwdc  12930  sqpweven  12931  2sqpwodd  12932  phimullem  12981  eulerthlem1  12983  eulerthlemfi  12984  eulerthlemrprm  12985  eulerthlemth  12988  hashgcdlem  12994  pclem0  13043  pclemub  13044  pclemdc  13045  pcprecl  13046  pcprendvds  13047  1arith  13124  elgz  13128  4sqlem13m  13160  4sqlem17  13164  4sqlem18  13165  ballotfilemelo  13200  ballotfileme  13214  ballotfilemscl  13225  ctiunctlemu1st  13303  ctiunctlemu2nd  13304  ctiunctlemudc  13306  ctiunctlemfo  13308  infpn2  13325  issgrp  13695  ismnddef  13708  gsumvallem2  13777  isgrp  13788  elnmz  13988  iscmn  14073  isrng  14208  issrg  14243  isring  14278  iscrng  14281  isnzr  14461  islring  14472  isrrg  14544  isdomn  14551  isdrngtap  14579  islmod  14600  psrbag  14976  psrbagconcl  14986  psr1clfi  15002  isxms  15475  isms  15477  ivthinclemlm  15658  ivthinclemum  15659  ivthinclemlopn  15660  ivthinclemlr  15661  ivthinclemuopn  15662  ivthinclemur  15663  ivthinclemdisj  15664  ivthinclemloc  15665  mpodvdsmulf1o  16018  lgslem2  16034  lgslem3  16035  lgsfcl2  16039  lfgredg2dom  16287  uspgredg2vlem  16375  uspgredg2v  16376  usgredg2vlem1  16377  usgredg2vlem2  16378  ushgredgedg  16381  ushgredgedgloop  16383  isclwwlknon  16585  s2elclwwlknon2  16591  0nninf  16952  nnsf  16953  peano4nninf  16954  nninfalllem1  16956  nninfself  16961  qdencn  16977