Theorem elrab 2963

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2202  {crab 2515

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rab 2520  df-v 2805

This theorem is referenced by:  elrab3  2964  elrabd  2965  elrab2  2966  ralrab  2968  rexrab  2970  rabsnt  3750  unimax  3932  ssintub  3951  intminss  3958  exmidexmid  4292  exmidsssnc  4299  rabxfrd  4572  ordtri2or2exmidlem  4630  onsucelsucexmidlem1  4632  sefvex  5669  ssimaex  5716  acexmidlem2  6025  elsuppfng  6420  elsuppfn  6421  elpmg  6876  ssfilem  7105  ssfilemd  7107  diffitest  7119  inffiexmid  7141  supubti  7241  suplubti  7242  ctssexmid  7392  sspw1or2  7446  exmidonfinlem  7447  finacn  7462  cc4f  7531  cc4n  7533  acnccim  7534  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemdisj  7983  suplocexprlemub  7986  nnindnn  8156  negf1o  8603  apsscn  8869  sup3exmid  9179  nnind  9201  peano2uz2  9631  peano5uzti  9632  dfuzi  9634  uzind  9635  uzind3  9637  eluz1  9803  uzind4  9866  supinfneg  9873  infsupneg  9874  eqreznegel  9892  elixx1  10176  elioo2  10200  elfz1  10293  zsupcl  10537  infssuzex  10539  infssuzcldc  10541  expcl2lemap  10859  expclzaplem  10871  expclzap  10872  expap0i  10879  expge0  10883  expge1  10884  hashennnuni  11087  wrdmap  11194  shftf  11453  reccn2ap  11936  dvdsdivcl  12474  divalgmod  12551  bitsval  12567  bitsfzolem  12578  bezoutlemsup  12643  dfgcd2  12648  uzwodc  12671  nnwosdc  12673  nninfctlemfo  12674  lcmgcdlem  12712  1nprm  12749  1idssfct  12750  isprm2  12752  phicl2  12849  hashdvds  12856  dvdsfi  12874  phisum  12876  odzval  12877  odzcllem  12878  odzdvds  12881  oddennn  13076  evenennn  13077  znnen  13082  ennnfonelemg  13087  ennnfonelemom  13092  ismhm  13607  issubm  13618  issubmd  13620  grplinv  13696  issubg  13823  isnsg  13852  isrim0  14239  issubrng  14277  issubrg  14299  islssm  14436  islssmg  14437  cnfldui  14668  mplelbascoe  14776  istopon  14807  epttop  14884  iscld  14897  isnei  14938  neipsm  14948  iscn  14991  iscnp  14993  txdis1cn  15072  ishmeo  15098  ispsmet  15117  ismet  15138  isxmet  15139  elblps  15184  elbl  15185  xmetxpbl  15302  reopnap  15340  divcnap  15359  elcncf  15367  cdivcncfap  15398  cnopnap  15405  divcncfap  15408  maxcncf  15409  mincncf  15410  ellimc3apf  15454  limccoap  15472  dvlemap  15474  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvrecap  15507  dveflem  15520  pellexlem3  15776  dvdsppwf1o  15786  lgsfle1  15811  lgsle1  15817  lgsdirprm  15836  lgsne0  15840  lgsquadlem1  15879  lgsquadlem2  15880  uhgrm  16002  upgrm  16024  upgr1or2  16025  umgredg2en  16033  umgrbien  16034  uhgredgm  16060  edgupgren  16065  edgumgren  16066  edgusgren  16087  usgruspgrben  16110  ushgredgedg  16150  ushgredgedgloop  16152  isclwwlk  16318  isclwwlkng  16330  clwwlknon  16353  eupth2lemsfi  16402  konigsberglem1  16412  konigsberglem4  16415  2omap  16698  pw1map  16700  subctctexmid  16705