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  9646  elrp  10056  repos  10372  zsupssdc  10673  bitsfzolem  12721  isprm  12887  oddpwdc  12952  sqpweven  12953  2sqpwodd  12954  phimullem  13003  eulerthlem1  13005  eulerthlemfi  13006  eulerthlemrprm  13007  eulerthlemth  13010  hashgcdlem  13016  pclem0  13065  pclemub  13066  pclemdc  13067  pcprecl  13068  pcprendvds  13069  1arith  13146  elgz  13150  4sqlem13m  13182  4sqlem17  13186  4sqlem18  13187  ballotfilemelo  13222  ballotfileme  13236  ballotfilemscl  13247  ctiunctlemu1st  13325  ctiunctlemu2nd  13326  ctiunctlemudc  13328  ctiunctlemfo  13330  infpn2  13347  issgrp  13718  ismnddef  13731  gsumvallem2  13800  isgrp  13811  elnmz  14011  iscmn  14096  isrng  14233  issrg  14269  isring  14304  iscrng  14307  isnzr  14488  islring  14499  isrrg  14571  isdomn  14578  isdrngtap  14606  islmod  14627  isassa  15002  psrbag  15053  psrbagconcl  15063  psr1clfi  15079  isxms  15552  isms  15554  ivthinclemlm  15735  ivthinclemum  15736  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemdisj  15741  ivthinclemloc  15742  mpodvdsmulf1o  16104  lgslem2  16120  lgslem3  16121  lgsfcl2  16125  lfgredg2dom  16373  uspgredg2vlem  16461  uspgredg2v  16462  usgredg2vlem1  16463  usgredg2vlem2  16464  ushgredgedg  16467  ushgredgedgloop  16469  isclwwlknon  16671  s2elclwwlknon2  16677  0nninf  17047  nnsf  17048  peano4nninf  17049  nninfalllem1  17051  nninfself  17056  qdencn  17072