Theorem elrab 2928

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 2347	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2347	. 2 ⊢ Ⅎ𝑥𝐵
3		nfv 1550	. 2 ⊢ Ⅎ𝑥𝜓
4		elrab.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	elrabf 2926	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1372   ∈ wcel 2175  {crab 2487

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rab 2492  df-v 2773

This theorem is referenced by:  elrab3  2929  elrabd  2930  elrab2  2931  ralrab  2933  rexrab  2935  rabsnt  3707  unimax  3883  ssintub  3902  intminss  3909  exmidexmid  4239  exmidsssnc  4246  rabxfrd  4514  ordtri2or2exmidlem  4572  onsucelsucexmidlem1  4574  sefvex  5591  ssimaex  5634  acexmidlem2  5931  elpmg  6741  ssfilem  6954  diffitest  6966  inffiexmid  6985  supubti  7083  suplubti  7084  ctssexmid  7234  exmidonfinlem  7283  finacn  7298  cc4f  7363  cc4n  7365  acnccim  7366  caucvgprlemladdfu  7772  caucvgprlemladdrl  7773  suplocexprlemmu  7813  suplocexprlemru  7814  suplocexprlemdisj  7815  suplocexprlemub  7818  nnindnn  7988  negf1o  8436  apsscn  8702  sup3exmid  9012  nnind  9034  peano2uz2  9462  peano5uzti  9463  dfuzi  9465  uzind  9466  uzind3  9468  eluz1  9634  uzind4  9691  supinfneg  9698  infsupneg  9699  eqreznegel  9717  elixx1  10001  elioo2  10025  elfz1  10117  zsupcl  10355  infssuzex  10357  infssuzcldc  10359  expcl2lemap  10677  expclzaplem  10689  expclzap  10690  expap0i  10697  expge0  10701  expge1  10702  hashennnuni  10905  wrdmap  11000  shftf  11060  reccn2ap  11543  dvdsdivcl  12080  divalgmod  12157  bitsval  12173  bitsfzolem  12184  bezoutlemsup  12249  dfgcd2  12254  uzwodc  12277  nnwosdc  12279  nninfctlemfo  12280  lcmgcdlem  12318  1nprm  12355  1idssfct  12356  isprm2  12358  phicl2  12455  hashdvds  12462  dvdsfi  12480  phisum  12482  odzval  12483  odzcllem  12484  odzdvds  12487  oddennn  12682  evenennn  12683  znnen  12688  ennnfonelemg  12693  ennnfonelemom  12698  ismhm  13211  issubm  13222  issubmd  13224  grplinv  13300  issubg  13427  isnsg  13456  isrim0  13841  issubrng  13879  issubrg  13901  islssm  14037  islssmg  14038  cnfldui  14269  mplelbascoe  14372  istopon  14403  epttop  14480  iscld  14493  isnei  14534  neipsm  14544  iscn  14587  iscnp  14589  txdis1cn  14668  ishmeo  14694  ispsmet  14713  ismet  14734  isxmet  14735  elblps  14780  elbl  14781  xmetxpbl  14898  reopnap  14936  divcnap  14955  elcncf  14963  cdivcncfap  14994  cnopnap  15001  divcncfap  15004  maxcncf  15005  mincncf  15006  ellimc3apf  15050  limccoap  15068  dvlemap  15070  dvidlemap  15081  dvidrelem  15082  dvidsslem  15083  dvcnp2cntop  15089  dvaddxxbr  15091  dvmulxxbr  15092  dvcoapbr  15097  dvcjbr  15098  dvrecap  15103  dveflem  15116  dvdsppwf1o  15379  lgsfle1  15404  lgsle1  15410  lgsdirprm  15429  lgsne0  15433  lgsquadlem1  15472  lgsquadlem2  15473  2omap  15796  subctctexmid  15801