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  4333  exmidsssnc  4340  rabxfrd  4615  ordtri2or2exmidlem  4673  onsucelsucexmidlem1  4675  sefvex  5716  ssimaex  5764  acexmidlem2  6082  elsuppfng  6482  elsuppfn  6483  elpmg  6938  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  2omap  7319  supubti  7340  suplubti  7341  ctssexmid  7491  sspw1or2  7545  exmidonfinlem  7546  finacn  7561  cc4f  7636  cc4n  7638  acnccim  7639  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemdisj  8088  suplocexprlemub  8091  nnindnn  8261  negf1o  8711  apsscn  8978  sup3exmid  9290  nnind  9323  peano2uz2  9758  peano5uzti  9759  dfuzi  9761  uzind  9762  uzind3  9764  eluz1  9935  uzind4  9998  supinfneg  10005  infsupneg  10006  eqreznegel  10024  elixx1  10310  elioo2  10334  elfz1  10427  zsupcl  10675  infssuzex  10677  infssuzcldc  10679  expcl2lemap  11003  expclzaplem  11015  expclzap  11016  expap0i  11023  expge0  11027  expge1  11028  hashennnuni  11234  hashfibclem  11298  wrdmap  11352  shftf  11611  reccn2ap  12098  dvdsdivcl  12636  divalgmod  12713  bitsval  12729  bitsfzolem  12740  bezoutlemsup  12805  dfgcd2  12810  uzwodc  12833  nnwosdc  12835  nninfctlemfo  12836  lcmgcdlem  12874  1nprm  12911  1idssfct  12912  isprm2  12914  phicl2  13015  hashdvds  13022  dvdsfi  13040  phisum  13042  odzval  13043  odzcllem  13044  odzdvds  13047  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemiex  13296  ballotfilemimin  13301  ballotfilemfrcn0  13325  ballotfilemirc  13327  ballotfilem7  13331  oddennn  13335  evenennn  13336  znnen  13341  ennnfonelemg  13346  ennnfonelemom  13351  ismhm  13821  issubm  13832  issubmd  13834  grplinv  13908  issubg  14029  isnsg  14058  elcntz  14148  elcntzsn  14151  isrim0  14552  issubrng  14591  issubrg  14613  ringunitsap0  14678  drnguiap  14693  islssm  14778  islssmg  14779  cnfldui  15008  rhmpsrfilem2  15157  mplelbascoe  15174  istopon  15205  epttop  15282  iscld  15295  isnei  15336  neipsm  15346  iscn  15389  iscnp  15391  txdis1cn  15470  ishmeo  15496  ispsmet  15515  ismet  15536  isxmet  15537  elblps  15582  elbl  15583  xmetxpbl  15700  reopnap  15738  divcnap  15757  elcncf  15765  cdivcncfap  15796  cnopnap  15803  divcncfap  15806  maxcncf  15807  mincncf  15808  ellimc3apf  15852  limccoap  15870  dvlemap  15872  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvrecap  15905  dveflem  15918  pellexlem3  16192  efnnfsumcl  16200  prmdvdsfi  16204  efchtqdvds  16226  dvdsppwf1o  16244  ppiqub  16254  lgsfle1  16294  lgsle1  16300  lgsdirprm  16319  lgsne0  16323  lgsquadlem1  16362  lgsquadlem2  16363  uhgrm  16485  upgrm  16507  upgr1or2  16508  umgredg2en  16516  umgrbien  16517  uhgredgm  16543  edgupgren  16548  edgumgren  16549  edgusgren  16570  usgruspgrben  16593  ushgredgedg  16633  ushgredgedgloop  16635  isclwwlk  16801  isclwwlkng  16813  clwwlknon  16836  eupth2lemsfi  16885  konigsberglem1  16895  konigsberglem4  16898  pw1map  17191  subctctexmid  17196  wexmiddiffilem  17209