Theorem elrab2 2919

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2164  {crab 2476

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-v 2762

This theorem is referenced by:  elrabsf  3024  pwnss  4188  regexmidlemm  4564  regexmidlem1  4565  reg2exmidlema  4566  tfis  4615  ctssdccl  7170  nninff  7181  nninfninc  7182  infnninf  7183  infnninfOLD  7184  nnnninf  7185  nnnninfeq  7187  nnnninfeq2  7188  nninfwlpoimlemg  7234  exmidaclem  7268  ltexprlemell  7658  ltexprlemelu  7659  cauappcvgprlemm  7705  cauappcvgprlemopl  7706  cauappcvgprlemlol  7707  cauappcvgprlemopu  7708  cauappcvgprlemupu  7709  cauappcvgprlemdisj  7711  cauappcvgprlemloc  7712  cauappcvgprlemladdfu  7714  cauappcvgprlemladdfl  7715  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem2  7720  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemopu  7731  caucvgprlemupu  7732  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemladdfu  7737  caucvgprlem2  7740  caucvgprprlemell  7745  caucvgprprlemelu  7746  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemexbt  7766  caucvgprprlem2  7770  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  axpre-suploclemres  7961  elz  9319  elrp  9721  repos  10036  zsupssdc  12091  isprm  12247  oddpwdc  12312  sqpweven  12313  2sqpwodd  12314  phimullem  12363  eulerthlem1  12365  eulerthlemfi  12366  eulerthlemrprm  12367  eulerthlemth  12370  hashgcdlem  12376  pclem0  12424  pclemub  12425  pclemdc  12426  pcprecl  12427  pcprendvds  12428  1arith  12505  elgz  12509  4sqlem13m  12541  4sqlem17  12545  4sqlem18  12546  ctiunctlemu1st  12591  ctiunctlemu2nd  12592  ctiunctlemudc  12594  ctiunctlemfo  12596  infpn2  12613  issgrp  12986  ismnddef  12999  gsumvallem2  13065  isgrp  13078  elnmz  13278  iscmn  13363  isrng  13430  issrg  13461  isring  13496  iscrng  13499  isnzr  13677  islring  13688  isrrg  13759  isdomn  13765  islmod  13787  psrbag  14155  isxms  14619  isms  14621  ivthinclemlm  14788  ivthinclemum  14789  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemdisj  14794  ivthinclemloc  14795  lgslem2  15117  lgslem3  15118  lgsfcl2  15122  0nninf  15494  nnsf  15495  peano4nninf  15496  nninfalllem1  15498  nninfself  15503  qdencn  15517