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  7451  nninff  7462  nninfninc  7463  infnninf  7464  infnninfOLD  7465  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  nninfwlpoimlemg  7515  exmidaclem  7564  ltexprlemell  7965  ltexprlemelu  7966  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemell  8052  caucvgprprlemelu  8053  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemexbt  8073  caucvgprprlem2  8077  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axpre-suploclemres  8268  elz  9650  elrp  10066  repos  10382  zsupssdc  10683  bitsfzolem  12737  isprm  12903  nnmaxpw  12969  sqpweven  12971  2sqpwodd  12972  phimullem  13023  eulerthlem1  13025  eulerthlemfi  13026  eulerthlemrprm  13027  eulerthlemth  13030  hashgcdlem  13036  pclem0  13085  pclemub  13086  pclemdc  13087  pcprecl  13088  pcprendvds  13089  1arith  13166  elgz  13170  4sqlem13m  13202  4sqlem17  13206  4sqlem18  13207  ballotfilemelo  13271  ballotfileme  13285  ballotfilemscl  13296  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  ctiunctlemudc  13377  ctiunctlemfo  13379  infpn2  13396  issgrp  13767  ismnddef  13780  gsumvallem2  13849  isgrp  13860  elnmz  14060  iscmn  14145  isrng  14282  issrg  14318  isring  14353  iscrng  14356  isnzr  14537  islring  14548  isrrg  14620  isdomn  14627  isdrngtap  14655  islmod  14676  isassa  15051  psrbag  15102  psrbagconcl  15112  psr1clfi  15128  isxms  15601  isms  15603  ivthinclemlm  15784  ivthinclemum  15785  ivthinclemlopn  15786  ivthinclemlr  15787  ivthinclemuopn  15788  ivthinclemur  15789  ivthinclemdisj  15790  ivthinclemloc  15791  zprmlogbaplem3  16136  mpodvdsmulf1o  16185  lgslem2  16218  lgslem3  16219  lgsfcl2  16223  lfgredg2dom  16471  uspgredg2vlem  16559  uspgredg2v  16560  usgredg2vlem1  16561  usgredg2vlem2  16562  ushgredgedg  16565  ushgredgedgloop  16567  isclwwlknon  16769  s2elclwwlknon2  16775  0nninf  17145  nnsf  17146  peano4nninf  17147  nninfalllem1  17149  nninfself  17154  qdencn  17170