Theorem elrab2 2896

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739

This theorem is referenced by:  elrabsf  3001  pwnss  4157  regexmidlemm  4529  regexmidlem1  4530  reg2exmidlema  4531  tfis  4580  ctssdccl  7105  nninff  7116  infnninf  7117  infnninfOLD  7118  nnnninf  7119  nnnninfeq  7121  nnnninfeq2  7122  nninfwlpoimlemg  7168  exmidaclem  7202  ltexprlemell  7592  ltexprlemelu  7593  cauappcvgprlemm  7639  cauappcvgprlemopl  7640  cauappcvgprlemlol  7641  cauappcvgprlemopu  7642  cauappcvgprlemupu  7643  cauappcvgprlemdisj  7645  cauappcvgprlemloc  7646  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  cauappcvgprlem2  7654  caucvgprlemm  7662  caucvgprlemopl  7663  caucvgprlemlol  7664  caucvgprlemopu  7665  caucvgprlemupu  7666  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemladdfu  7671  caucvgprlem2  7674  caucvgprprlemell  7679  caucvgprprlemelu  7680  caucvgprprlemml  7688  caucvgprprlemmu  7689  caucvgprprlemexbt  7700  caucvgprprlem2  7704  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  axpre-suploclemres  7895  elz  9249  elrp  9649  repos  9964  zsupssdc  11945  isprm  12099  oddpwdc  12164  sqpweven  12165  2sqpwodd  12166  phimullem  12215  eulerthlem1  12217  eulerthlemfi  12218  eulerthlemrprm  12219  eulerthlemth  12222  hashgcdlem  12228  pclem0  12276  pclemub  12277  pclemdc  12278  pcprecl  12279  pcprendvds  12280  1arith  12355  elgz  12359  ctiunctlemu1st  12425  ctiunctlemu2nd  12426  ctiunctlemudc  12428  ctiunctlemfo  12430  infpn2  12447  issgrp  12739  ismnddef  12749  isgrp  12811  iscmn  12996  issrg  13048  isring  13083  iscrng  13086  isnzr  13224  islring  13232  isxms  13733  isms  13735  ivthinclemlm  13894  ivthinclemum  13895  ivthinclemlopn  13896  ivthinclemlr  13897  ivthinclemuopn  13898  ivthinclemur  13899  ivthinclemdisj  13900  ivthinclemloc  13901  lgslem2  14184  lgslem3  14185  lgsfcl2  14189  0nninf  14524  nnsf  14525  peano4nninf  14526  nninfalllem1  14528  nninfself  14533  qdencn  14546