MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfuni Structured version   Visualization version   GIF version

Theorem nfuni 4368
Description: Bound-variable hypothesis builder for union. (Contributed by NM, 30-Dec-1996.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Hypothesis
Ref Expression
nfuni.1 𝑥𝐴
Assertion
Ref Expression
nfuni 𝑥 𝐴

Proof of Theorem nfuni
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfuni2 4364 . 2 𝐴 = {𝑦 ∣ ∃𝑧𝐴 𝑦𝑧}
2 nfuni.1 . . . 4 𝑥𝐴
3 nfv 1828 . . . 4 𝑥 𝑦𝑧
42, 3nfrex 2985 . . 3 𝑥𝑧𝐴 𝑦𝑧
54nfab 2750 . 2 𝑥{𝑦 ∣ ∃𝑧𝐴 𝑦𝑧}
61, 5nfcxfr 2744 1 𝑥 𝐴
Colors of variables: wff setvar class
Syntax hints:  {cab 2591  wnfc 2733  wrex 2892   cuni 4362
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-uni 4363
This theorem is referenced by:  nfiota1  5752  nfwrecs  7269  nfsup  8213  ptunimpt  21146  disjabrex  28579  disjabrexf  28580  nfesum1  29231  nfesum2  29232  bnj1398  30158  bnj1446  30169  bnj1447  30170  bnj1448  30171  bnj1466  30177  bnj1467  30178  bnj1519  30189  bnj1520  30190  bnj1525  30193  bnj1523  30195  dfon2lem3  30736  bj-xnex  32044  mptsnunlem  32160  ptrest  32377  heibor1  32578  nfunidALT2  33073  nfunidALT  33074  disjinfi  38174  stoweidlem28  38721  stoweidlem59  38752  fourierdlem80  38879  smfresal  39473  smfpimbor1lem2  39484
  Copyright terms: Public domain W3C validator