Theorem elrab2 2936

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1373   ∈ wcel 2177  {crab 2489

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-rab 2494  df-v 2775

This theorem is referenced by:  elrabsf  3041  pwnss  4211  regexmidlemm  4588  regexmidlem1  4589  reg2exmidlema  4590  tfis  4639  ctssdccl  7228  nninff  7239  nninfninc  7240  infnninf  7241  infnninfOLD  7242  nnnninf  7243  nnnninfeq  7245  nnnninfeq2  7246  nninfwlpoimlemg  7292  exmidaclem  7336  ltexprlemell  7731  ltexprlemelu  7732  cauappcvgprlemm  7778  cauappcvgprlemopl  7779  cauappcvgprlemlol  7780  cauappcvgprlemopu  7781  cauappcvgprlemupu  7782  cauappcvgprlemdisj  7784  cauappcvgprlemloc  7785  cauappcvgprlemladdfu  7787  cauappcvgprlemladdfl  7788  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  cauappcvgprlem2  7793  caucvgprlemm  7801  caucvgprlemopl  7802  caucvgprlemlol  7803  caucvgprlemopu  7804  caucvgprlemupu  7805  caucvgprlemdisj  7807  caucvgprlemloc  7808  caucvgprlemladdfu  7810  caucvgprlem2  7813  caucvgprprlemell  7818  caucvgprprlemelu  7819  caucvgprprlemml  7827  caucvgprprlemmu  7828  caucvgprprlemexbt  7839  caucvgprprlem2  7843  suplocsrlemb  7939  suplocsrlempr  7940  suplocsrlem  7941  axpre-suploclemres  8034  elz  9394  elrp  9797  repos  10112  zsupssdc  10403  bitsfzolem  12340  isprm  12506  oddpwdc  12571  sqpweven  12572  2sqpwodd  12573  phimullem  12622  eulerthlem1  12624  eulerthlemfi  12625  eulerthlemrprm  12626  eulerthlemth  12629  hashgcdlem  12635  pclem0  12684  pclemub  12685  pclemdc  12686  pcprecl  12687  pcprendvds  12688  1arith  12765  elgz  12769  4sqlem13m  12801  4sqlem17  12805  4sqlem18  12806  ctiunctlemu1st  12880  ctiunctlemu2nd  12881  ctiunctlemudc  12883  ctiunctlemfo  12885  infpn2  12902  issgrp  13310  ismnddef  13325  gsumvallem2  13400  isgrp  13413  elnmz  13619  iscmn  13704  isrng  13771  issrg  13802  isring  13837  iscrng  13840  isnzr  14018  islring  14029  isrrg  14100  isdomn  14106  islmod  14128  psrbag  14506  psr1clfi  14525  isxms  14998  isms  15000  ivthinclemlm  15181  ivthinclemum  15182  ivthinclemlopn  15183  ivthinclemlr  15184  ivthinclemuopn  15185  ivthinclemur  15186  ivthinclemdisj  15187  ivthinclemloc  15188  mpodvdsmulf1o  15537  lgslem2  15553  lgslem3  15554  lgsfcl2  15558  0nninf  16082  nnsf  16083  peano4nninf  16084  nninfalllem1  16086  nninfself  16091  qdencn  16107