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

Theorem nfuni 4433
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 4429 . 2 𝐴 = {𝑦 ∣ ∃𝑧𝐴 𝑦𝑧}
2 nfuni.1 . . . 4 𝑥𝐴
3 nfv 1841 . . . 4 𝑥 𝑦𝑧
42, 3nfrex 3004 . . 3 𝑥𝑧𝐴 𝑦𝑧
54nfab 2766 . 2 𝑥{𝑦 ∣ ∃𝑧𝐴 𝑦𝑧}
61, 5nfcxfr 2760 1 𝑥 𝐴
Colors of variables: wff setvar class
Syntax hints:  {cab 2606  wnfc 2749  wrex 2910   cuni 4427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-uni 4428
This theorem is referenced by:  nfiota1  5841  nfwrecs  7394  nfsup  8342  ptunimpt  21379  disjabrex  29367  disjabrexf  29368  nfesum1  30076  nfesum2  30077  bnj1398  31076  bnj1446  31087  bnj1447  31088  bnj1448  31089  bnj1466  31095  bnj1467  31096  bnj1519  31107  bnj1520  31108  bnj1525  31111  bnj1523  31113  dfon2lem3  31664  mptsnunlem  33156  ptrest  33379  heibor1  33580  nfunidALT2  34075  nfunidALT  34076  disjinfi  39196  stoweidlem28  40008  stoweidlem59  40039  fourierdlem80  40166  smfresal  40758  smfpimbor1lem2  40769  nfsetrecs  42198
  Copyright terms: Public domain W3C validator