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

Theorem nfuni 4712
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 4708 . 2 𝐴 = {𝑦 ∣ ∃𝑧𝐴 𝑦𝑧}
2 nfuni.1 . . . 4 𝑥𝐴
3 nfv 1873 . . . 4 𝑥 𝑦𝑧
42, 3nfrex 3247 . . 3 𝑥𝑧𝐴 𝑦𝑧
54nfab 2932 . 2 𝑥{𝑦 ∣ ∃𝑧𝐴 𝑦𝑧}
61, 5nfcxfr 2924 1 𝑥 𝐴
Colors of variables: wff setvar class
Syntax hints:  {cab 2753  wnfc 2910  wrex 3083   cuni 4706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-uni 4707
This theorem is referenced by:  nfiota1  6148  nfwrecs  7745  nfsup  8702  ptunimpt  21897  disjabrex  30088  disjabrexf  30089  fnpreimac  30168  nfesum1  30900  nfesum2  30901  bnj1398  31912  bnj1446  31923  bnj1447  31924  bnj1448  31925  bnj1466  31931  bnj1467  31932  bnj1519  31943  bnj1520  31944  bnj1525  31947  bnj1523  31949  dfon2lem3  32490  nffrecs  32581  mptsnunlem  33996  ptrest  34280  heibor1  34478  nfunidALT2  35498  nfunidALT  35499  disjinfi  40824  stoweidlem28  41690  stoweidlem59  41721  fourierdlem80  41848  smfresal  42440  smfpimbor1lem2  42451  nfafv2  42769  nfsetrecs  44096
  Copyright terms: Public domain W3C validator