Theorem elrab 2881

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1343   ∈ wcel 2136  {crab 2447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-rab 2452  df-v 2727

This theorem is referenced by:  elrab3  2882  elrabd  2883  elrab2  2884  ralrab  2886  rexrab  2888  rabsnt  3650  unimax  3822  ssintub  3841  intminss  3848  exmidexmid  4174  exmidsssnc  4181  rabxfrd  4446  ordtri2or2exmidlem  4502  onsucelsucexmidlem1  4504  sefvex  5506  ssimaex  5546  acexmidlem2  5838  elpmg  6626  ssfilem  6837  diffitest  6849  inffiexmid  6868  supubti  6960  suplubti  6961  ctssexmid  7110  exmidonfinlem  7145  cc4f  7206  cc4n  7208  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  suplocexprlemmu  7655  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemub  7660  nnindnn  7830  negf1o  8276  apsscn  8541  sup3exmid  8848  nnind  8869  peano2uz2  9294  peano5uzti  9295  dfuzi  9297  uzind  9298  uzind3  9300  eluz1  9466  uzind4  9522  supinfneg  9529  infsupneg  9530  eqreznegel  9548  elixx1  9829  elioo2  9853  elfz1  9945  expcl2lemap  10463  expclzaplem  10475  expclzap  10476  expap0i  10483  expge0  10487  expge1  10488  hashennnuni  10688  shftf  10768  reccn2ap  11250  dvdsdivcl  11784  divalgmod  11860  zsupcl  11876  infssuzex  11878  infssuzcldc  11880  bezoutlemsup  11938  dfgcd2  11943  uzwodc  11966  nnwosdc  11968  lcmcllem  11995  lcmledvds  11998  lcmgcdlem  12005  1nprm  12042  1idssfct  12043  isprm2  12045  phicl2  12142  hashdvds  12149  phisum  12168  odzval  12169  odzcllem  12170  odzdvds  12173  oddennn  12321  evenennn  12322  znnen  12327  ennnfonelemg  12332  ennnfonelemom  12337  istopon  12611  epttop  12690  iscld  12703  isnei  12744  neipsm  12754  iscn  12797  iscnp  12799  txdis1cn  12878  ishmeo  12904  ispsmet  12923  ismet  12944  isxmet  12945  elblps  12990  elbl  12991  xmetxpbl  13108  reopnap  13138  divcnap  13155  elcncf  13160  cdivcncfap  13187  cnopnap  13194  ellimc3apf  13229  limccoap  13247  dvlemap  13249  dvidlemap  13260  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277  dveflem  13287  lgsfle1  13510  lgsle1  13516  lgsdirprm  13535  lgsne0  13539  subctctexmid  13841