Theorem elrab 2920

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2167  {crab 2479

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-v 2765

This theorem is referenced by:  elrab3  2921  elrabd  2922  elrab2  2923  ralrab  2925  rexrab  2927  rabsnt  3698  unimax  3874  ssintub  3893  intminss  3900  exmidexmid  4230  exmidsssnc  4237  rabxfrd  4505  ordtri2or2exmidlem  4563  onsucelsucexmidlem1  4565  sefvex  5582  ssimaex  5625  acexmidlem2  5922  elpmg  6732  ssfilem  6945  diffitest  6957  inffiexmid  6976  supubti  7074  suplubti  7075  ctssexmid  7225  exmidonfinlem  7274  finacn  7289  cc4f  7354  cc4n  7356  acnccim  7357  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemub  7809  nnindnn  7979  negf1o  8427  apsscn  8693  sup3exmid  9003  nnind  9025  peano2uz2  9452  peano5uzti  9453  dfuzi  9455  uzind  9456  uzind3  9458  eluz1  9624  uzind4  9681  supinfneg  9688  infsupneg  9689  eqreznegel  9707  elixx1  9991  elioo2  10015  elfz1  10107  zsupcl  10340  infssuzex  10342  infssuzcldc  10344  expcl2lemap  10662  expclzaplem  10674  expclzap  10675  expap0i  10682  expge0  10686  expge1  10687  hashennnuni  10890  wrdmap  10985  shftf  11014  reccn2ap  11497  dvdsdivcl  12034  divalgmod  12111  bitsval  12127  bitsfzolem  12138  bezoutlemsup  12203  dfgcd2  12208  uzwodc  12231  nnwosdc  12233  nninfctlemfo  12234  lcmgcdlem  12272  1nprm  12309  1idssfct  12310  isprm2  12312  phicl2  12409  hashdvds  12416  dvdsfi  12434  phisum  12436  odzval  12437  odzcllem  12438  odzdvds  12441  oddennn  12636  evenennn  12637  znnen  12642  ennnfonelemg  12647  ennnfonelemom  12652  ismhm  13165  issubm  13176  issubmd  13178  grplinv  13254  issubg  13381  isnsg  13410  isrim0  13795  issubrng  13833  issubrg  13855  islssm  13991  islssmg  13992  cnfldui  14223  mplelbascoe  14326  istopon  14357  epttop  14434  iscld  14447  isnei  14488  neipsm  14498  iscn  14541  iscnp  14543  txdis1cn  14622  ishmeo  14648  ispsmet  14667  ismet  14688  isxmet  14689  elblps  14734  elbl  14735  xmetxpbl  14852  reopnap  14890  divcnap  14909  elcncf  14917  cdivcncfap  14948  cnopnap  14955  divcncfap  14958  maxcncf  14959  mincncf  14960  ellimc3apf  15004  limccoap  15022  dvlemap  15024  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvrecap  15057  dveflem  15070  dvdsppwf1o  15333  lgsfle1  15358  lgsle1  15364  lgsdirprm  15383  lgsne0  15387  lgsquadlem1  15426  lgsquadlem2  15427  2omap  15750  subctctexmid  15755