Theorem elrab2 2894

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2146  {crab 2457

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-rab 2462  df-v 2737

This theorem is referenced by:  elrabsf  2999  pwnss  4154  regexmidlemm  4525  regexmidlem1  4526  reg2exmidlema  4527  tfis  4576  ctssdccl  7100  nninff  7111  infnninf  7112  infnninfOLD  7113  nnnninf  7114  nnnninfeq  7116  nnnninfeq2  7117  nninfwlpoimlemg  7163  exmidaclem  7197  ltexprlemell  7572  ltexprlemelu  7573  cauappcvgprlemm  7619  cauappcvgprlemopl  7620  cauappcvgprlemlol  7621  cauappcvgprlemopu  7622  cauappcvgprlemupu  7623  cauappcvgprlemdisj  7625  cauappcvgprlemloc  7626  cauappcvgprlemladdfu  7628  cauappcvgprlemladdfl  7629  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  cauappcvgprlem2  7634  caucvgprlemm  7642  caucvgprlemopl  7643  caucvgprlemlol  7644  caucvgprlemopu  7645  caucvgprlemupu  7646  caucvgprlemdisj  7648  caucvgprlemloc  7649  caucvgprlemladdfu  7651  caucvgprlem2  7654  caucvgprprlemell  7659  caucvgprprlemelu  7660  caucvgprprlemml  7668  caucvgprprlemmu  7669  caucvgprprlemexbt  7680  caucvgprprlem2  7684  suplocsrlemb  7780  suplocsrlempr  7781  suplocsrlem  7782  axpre-suploclemres  7875  elz  9228  elrp  9626  repos  9941  zsupssdc  11922  isprm  12076  oddpwdc  12141  sqpweven  12142  2sqpwodd  12143  phimullem  12192  eulerthlem1  12194  eulerthlemfi  12195  eulerthlemrprm  12196  eulerthlemth  12199  hashgcdlem  12205  pclem0  12253  pclemub  12254  pclemdc  12255  pcprecl  12256  pcprendvds  12257  1arith  12332  elgz  12336  ctiunctlemu1st  12402  ctiunctlemu2nd  12403  ctiunctlemudc  12405  ctiunctlemfo  12407  infpn2  12424  issgrp  12684  ismnddef  12694  isgrp  12754  iscmn  12904  issrg  12954  isring  12989  iscrng  12992  isxms  13531  isms  13533  ivthinclemlm  13692  ivthinclemum  13693  ivthinclemlopn  13694  ivthinclemlr  13695  ivthinclemuopn  13696  ivthinclemur  13697  ivthinclemdisj  13698  ivthinclemloc  13699  lgslem2  13982  lgslem3  13983  lgsfcl2  13987  0nninf  14323  nnsf  14324  peano4nninf  14325  nninfalllem1  14327  nninfself  14332  qdencn  14345