Theorem elrab 2982

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {crab 2532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is used by:  elrab3  2983  elrabd  2984  elrab2  2985  ralrab  2987  rexrab  2989  rabsnt  3786  unimax  3969  ssintub  3988  intminss  3995  exmidexmid  4335  exmidsssnc  4342  rabxfrd  4617  ordtri2or2exmidlem  4675  onsucelsucexmidlem1  4677  sefvex  5719  ssimaex  5767  acexmidlem2  6085  elsuppfng  6486  elsuppfn  6487  elpmg  6943  ssfilem  7183  ssfilemd  7185  diffitest  7197  inffiexmid  7219  2omap  7324  supubti  7345  suplubti  7346  ctssexmid  7496  sspw1or2  7550  exmidonfinlem  7551  finacn  7566  cc4f  7641  cc4n  7643  acnccim  7644  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemub  8096  nnindnn  8266  negf1o  8716  apsscn  8983  sup3exmid  9295  nnind  9329  peano2uz2  9763  peano5uzti  9764  dfuzi  9766  uzind  9767  uzind3  9769  eluz1  9940  uzind4  10003  supinfneg  10010  infsupneg  10011  eqreznegel  10029  elixx1  10315  elioo2  10339  elfz1  10432  zsupcl  10680  infssuzex  10682  infssuzcldc  10684  expcl2lemap  11008  expclzaplem  11020  expclzap  11021  expap0i  11028  expge0  11032  expge1  11033  hashennnuni  11239  hashfibclem  11303  wrdmap  11357  shftf  11616  reccn2ap  12103  dvdsdivcl  12641  divalgmod  12718  bitsval  12734  bitsfzolem  12745  bezoutlemsup  12810  dfgcd2  12815  uzwodc  12838  nnwosdc  12840  nninfctlemfo  12841  lcmgcdlem  12879  1nprm  12916  1idssfct  12917  isprm2  12919  phicl2  13020  hashdvds  13027  dvdsfi  13045  phisum  13047  odzval  13048  odzcllem  13049  odzdvds  13052  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemiex  13301  ballotfilemimin  13306  ballotfilemfrcn0  13330  ballotfilemirc  13332  ballotfilem7  13336  oddennn  13340  evenennn  13341  znnen  13346  ennnfonelemg  13351  ennnfonelemom  13356  ismhm  13826  issubm  13837  issubmd  13839  grplinv  13913  issubg  14034  isnsg  14063  elcntz  14153  elcntzsn  14156  isrim0  14576  issubrng  14615  issubrg  14637  ringunitsap0  14702  drnguiap  14717  islssm  14802  islssmg  14803  cnfldui  15032  gsumbagdiaglem  15184  rhmpsrfilem2  15194  psrlidmfi  15208  psrridmfi  15209  psrass1fi  15210  istopon  15256  epttop  15333  iscld  15346  isnei  15387  neipsm  15397  iscn  15440  iscnp  15442  txdis1cn  15521  ishmeo  15547  ispsmet  15566  ismet  15587  isxmet  15588  elblps  15633  elbl  15634  xmetxpbl  15751  reopnap  15789  divcnap  15808  elcncf  15816  cdivcncfap  15847  cnopnap  15854  divcncfap  15857  maxcncf  15858  mincncf  15859  ellimc3apf  15903  limccoap  15921  dvlemap  15923  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcnp2cntop  15942  dvaddxxbr  15944  dvmulxxbr  15945  dvcoapbr  15950  dvcjbr  15951  dvrecap  15956  dveflem  15969  pellexlem3  16248  efnnfsumcl  16256  prmdvdsfi  16260  efchtqdvds  16282  dvdsppwf1o  16300  ppiqub  16310  lgsfle1  16350  lgsle1  16356  lgsdirprm  16375  lgsne0  16379  lgsquadlem1  16418  lgsquadlem2  16419  uhgrm  16541  upgrm  16563  upgr1or2  16564  umgredg2en  16572  umgrbien  16573  uhgredgm  16599  edgupgren  16604  edgumgren  16605  edgusgren  16626  usgruspgrben  16649  ushgredgedg  16689  ushgredgedgloop  16691  isclwwlk  16857  isclwwlkng  16869  clwwlknon  16892  eupth2lemsfi  16941  konigsberglem1  16951  konigsberglem4  16954  pw1map  17247  subctctexmid  17252  wexmiddiffilem  17265