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 ⊢ (𝐴 ∈ 𝐶 ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {crab 2532

This proof depends on 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 proof 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 used by:  elrabsf  3090  pwnss  4296  regexmidlemm  4679  regexmidlem1  4680  reg2exmidlema  4681  tfis  4730  ctssdccl  7452  nninff  7463  nninfninc  7464  infnninf  7465  infnninfOLD  7466  nnnninf  7467  nnnninfeq  7469  nnnninfeq2  7470  nninfwlpoimlemg  7516  exmidaclem  7565  ltexprlemell  7966  ltexprlemelu  7967  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemopu  8016  cauappcvgprlemupu  8017  cauappcvgprlemdisj  8019  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem2  8028  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemopu  8039  caucvgprlemupu  8040  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemell  8053  caucvgprprlemelu  8054  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemexbt  8074  caucvgprprlem2  8078  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  axpre-suploclemres  8269  elz  9651  elrp  10067  repos  10383  zsupssdc  10684  bitsfzolem  12740  isprm  12906  nnmaxpw  12972  sqpweven  12974  2sqpwodd  12975  phimullem  13026  eulerthlem1  13028  eulerthlemfi  13029  eulerthlemrprm  13030  eulerthlemth  13033  hashgcdlem  13039  pclem0  13088  pclemub  13089  pclemdc  13090  pcprecl  13091  pcprendvds  13092  1arith  13169  elgz  13173  4sqlem13m  13205  4sqlem17  13209  4sqlem18  13210  ballotfilemelo  13274  ballotfileme  13288  ballotfilemscl  13299  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  ctiunctlemudc  13380  ctiunctlemfo  13382  infpn2  13399  issgrp  13771  ismnddef  13784  gsumvallem2  13853  isgrp  13864  elnmz  14064  iscmn  14180  isrng  14317  issrg  14353  isring  14388  iscrng  14391  isnzr  14572  islring  14583  isrrg  14655  isdomn  14662  isdrngtap  14690  islmod  14711  isassa  15086  psrbag  15137  psrbagconcl  15148  psr1clfi  15170  isxms  15643  isms  15645  ivthinclemlm  15826  ivthinclemum  15827  ivthinclemlopn  15828  ivthinclemlr  15829  ivthinclemuopn  15830  ivthinclemur  15831  ivthinclemdisj  15832  ivthinclemloc  15833  zprmlogbaplem3  16178  mpodvdsmulf1o  16245  lgslem2  16286  lgslem3  16287  lgsfcl2  16291  lfgredg2dom  16539  uspgredg2vlem  16627  uspgredg2v  16628  usgredg2vlem1  16629  usgredg2vlem2  16630  ushgredgedg  16633  ushgredgedgloop  16635  isclwwlknon  16837  s2elclwwlknon2  16843  0nninf  17213  nnsf  17214  peano4nninf  17215  nninfalllem1  17217  nninfself  17222  qdencn  17238