Theorem elrab 2959

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2801

This theorem is referenced by:  elrab3  2960  elrabd  2961  elrab2  2962  ralrab  2964  rexrab  2966  rabsnt  3741  unimax  3922  ssintub  3941  intminss  3948  exmidexmid  4280  exmidsssnc  4287  rabxfrd  4560  ordtri2or2exmidlem  4618  onsucelsucexmidlem1  4620  sefvex  5650  ssimaex  5697  acexmidlem2  6004  elpmg  6819  ssfilem  7045  diffitest  7057  inffiexmid  7079  supubti  7177  suplubti  7178  ctssexmid  7328  exmidonfinlem  7382  finacn  7397  cc4f  7466  cc4n  7468  acnccim  7469  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  suplocexprlemmu  7916  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemub  7921  nnindnn  8091  negf1o  8539  apsscn  8805  sup3exmid  9115  nnind  9137  peano2uz2  9565  peano5uzti  9566  dfuzi  9568  uzind  9569  uzind3  9571  eluz1  9737  uzind4  9795  supinfneg  9802  infsupneg  9803  eqreznegel  9821  elixx1  10105  elioo2  10129  elfz1  10221  zsupcl  10463  infssuzex  10465  infssuzcldc  10467  expcl2lemap  10785  expclzaplem  10797  expclzap  10798  expap0i  10805  expge0  10809  expge1  10810  hashennnuni  11013  wrdmap  11116  shftf  11356  reccn2ap  11839  dvdsdivcl  12376  divalgmod  12453  bitsval  12469  bitsfzolem  12480  bezoutlemsup  12545  dfgcd2  12550  uzwodc  12573  nnwosdc  12575  nninfctlemfo  12576  lcmgcdlem  12614  1nprm  12651  1idssfct  12652  isprm2  12654  phicl2  12751  hashdvds  12758  dvdsfi  12776  phisum  12778  odzval  12779  odzcllem  12780  odzdvds  12783  oddennn  12978  evenennn  12979  znnen  12984  ennnfonelemg  12989  ennnfonelemom  12994  ismhm  13509  issubm  13520  issubmd  13522  grplinv  13598  issubg  13725  isnsg  13754  isrim0  14140  issubrng  14178  issubrg  14200  islssm  14336  islssmg  14337  cnfldui  14568  mplelbascoe  14671  istopon  14702  epttop  14779  iscld  14792  isnei  14833  neipsm  14843  iscn  14886  iscnp  14888  txdis1cn  14967  ishmeo  14993  ispsmet  15012  ismet  15033  isxmet  15034  elblps  15079  elbl  15080  xmetxpbl  15197  reopnap  15235  divcnap  15254  elcncf  15262  cdivcncfap  15293  cnopnap  15300  divcncfap  15303  maxcncf  15304  mincncf  15305  ellimc3apf  15349  limccoap  15367  dvlemap  15369  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvrecap  15402  dveflem  15415  dvdsppwf1o  15678  lgsfle1  15703  lgsle1  15709  lgsdirprm  15728  lgsne0  15732  lgsquadlem1  15771  lgsquadlem2  15772  uhgrm  15893  upgrm  15915  upgr1or2  15916  umgredg2en  15924  umgrbien  15925  uhgredgm  15949  edgupgren  15954  edgumgren  15955  edgusgren  15976  usgruspgrben  15999  ushgredgedg  16039  ushgredgedgloop  16041  isclwwlk  16132  2omap  16418  pw1map  16420  subctctexmid  16425