Theorem elrab2 2843

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ∈ wcel 1480  {crab 2420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rab 2425  df-v 2688

This theorem is referenced by:  elrabsf  2947  pwnss  4083  regexmidlemm  4447  regexmidlem1  4448  reg2exmidlema  4449  tfis  4497  ctssdccl  6996  infnninf  7022  nnnninf  7023  exmidaclem  7064  ltexprlemell  7406  ltexprlemelu  7407  cauappcvgprlemm  7453  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemopu  7456  cauappcvgprlemupu  7457  cauappcvgprlemdisj  7459  cauappcvgprlemloc  7460  cauappcvgprlemladdfu  7462  cauappcvgprlemladdfl  7463  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem2  7468  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemopu  7479  caucvgprlemupu  7480  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprlem2  7488  caucvgprprlemell  7493  caucvgprprlemelu  7494  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemexbt  7514  caucvgprprlem2  7518  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axpre-suploclemres  7709  elz  9056  elrp  9443  repos  9753  isprm  11790  oddpwdc  11852  sqpweven  11853  2sqpwodd  11854  phimullem  11901  hashgcdlem  11903  ctiunctlemu1st  11947  ctiunctlemu2nd  11948  ctiunctlemudc  11950  ctiunctlemfo  11952  isxms  12620  isms  12622  ivthinclemlm  12781  ivthinclemum  12782  ivthinclemlopn  12783  ivthinclemlr  12784  ivthinclemuopn  12785  ivthinclemur  12786  ivthinclemdisj  12787  ivthinclemloc  12788  0nninf  13197  nninff  13198  nnsf  13199  peano4nninf  13200  nninfalllemn  13202  nninfalllem1  13203  nninfself  13209  qdencn  13222