Theorem elrab 2771

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)

Hypothesis

Ref	Expression
elrab.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elrab	⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		nfcv 2228	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2228	. 2 ⊢ Ⅎ𝑥𝐵
3		nfv 1466	. 2 ⊢ Ⅎ𝑥𝜓
4		elrab.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	elrabf 2769	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   = wceq 1289   ∈ wcel 1438  {crab 2363

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rab 2368  df-v 2621

This theorem is referenced by:  elrab3  2772  elrabd  2773  elrab2  2774  ralrab  2776  rexrab  2778  rabsnt  3517  unimax  3687  ssintub  3706  intminss  3713  exmidexmid  4031  rabxfrd  4291  ordtri2or2exmidlem  4342  onsucelsucexmidlem1  4344  sefvex  5326  ssimaex  5365  acexmidlem2  5649  elpmg  6421  ssfilem  6591  diffitest  6603  inffiexmid  6622  supubti  6694  suplubti  6695  caucvgprlemladdfu  7236  caucvgprlemladdrl  7237  nnindnn  7428  negf1o  7860  nnind  8438  peano2uz2  8853  peano5uzti  8854  dfuzi  8856  uzind  8857  uzind3  8859  eluz1  9023  uzind4  9076  supinfneg  9083  infsupneg  9084  eqreznegel  9099  elixx1  9315  elioo2  9339  elfz1  9429  expcl2lemap  9967  expclzaplem  9979  expclzap  9980  expap0i  9987  expge0  9991  expge1  9992  hashennnuni  10187  shftf  10264  dvdsdivcl  11129  divalgmod  11205  zsupcl  11221  infssuzex  11223  infssuzcldc  11225  bezoutlemsup  11276  dfgcd2  11281  lcmcllem  11327  lcmledvds  11330  lcmgcdlem  11337  1nprm  11374  1idssfct  11375  isprm2  11377  phicl2  11468  hashdvds  11475  oddennn  11483  evenennn  11484  znnen  11489  istopon  11610  elcncf  11629