Theorem nfsbcw 3795

Description: Bound-variable hypothesis builder for class substitution. Version of nfsbc 3798 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 7-Sep-2014.) Avoid ax-13 2365. (Revised by Gino Giotto, 10-Jan-2024.)

Hypotheses

Ref	Expression
nfsbcw.1	⊢ Ⅎ𝑥𝐴
nfsbcw.2	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfsbcw	⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfsbcw

Step	Hyp	Ref	Expression
1		nftru 1798	. . 3 ⊢ Ⅎ𝑦⊤
2		nfsbcw.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfsbcw.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfsbcdw 3794	. 2 ⊢ (⊤ → Ⅎ𝑥[𝐴 / 𝑦]𝜑)
7	6	mptru 1540	1 ⊢ Ⅎ𝑥[𝐴 / 𝑦]𝜑

Syntax hints:  ⊤wtru 1534  Ⅎwnf 1777  Ⅎwnfc 2875  [wsbc 3773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-sbc 3774

This theorem is referenced by:  opelopabgf  5542  opelopabf  5547  ralrnmptw  7102  elovmporab  7666  elovmporab1w  7667  ovmpt3rabdm  7679  elovmpt3rab1  7680  dfopab2  8056  dfoprab3s  8057  ralxpes  8140  ralxp3es  8143  frpoins3xpg  8144  frpoins3xp3g  8145  mpoxopoveq  8224  elmptrab  23771  bnj1445  34787  bnj1446  34788  bnj1467  34797  indexa  37318  sdclem1  37328  sbcalf  37699  sbcexf  37700  sbccomieg  42322  rexrabdioph  42323  or2expropbilem2  46520  or2expropbi  46521  ich2exprop  46915  ichnreuop  46916  reuopreuprim  46970

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »