Theorem elixp2 8835

Description: Membership in an infinite Cartesian product. See df-ixp 8832 for discussion of the notation. (Contributed by NM, 28-Sep-2006.)

Assertion

Ref	Expression
elixp2	⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem elixp2

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fneq1 6577	. . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓 Fn 𝐴 ↔ 𝐹 Fn 𝐴))
2		fveq1 6825	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥))
3	2	eleq1d 2813	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ∈ 𝐵 ↔ (𝐹‘𝑥) ∈ 𝐵))
4	3	ralbidv 3152	. . . . 5 ⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5	1, 4	anbi12d 632	. . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)))
6		dfixp 8833	. . . 4 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)}
7	5, 6	elab2g 3638	. . 3 ⊢ (𝐹 ∈ V → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)))
8	7	pm5.32i 574	. 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)))
9		elex 3459	. . 3 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 ∈ V)
10	9	pm4.71ri 560	. 2 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐵))
11		3anass 1094	. 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)))
12	8, 10, 11	3bitr4i 303	1 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3438   Fn wfn 6481  ‘cfv 6486  Xcixp 8831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fn 6489  df-fv 6494  df-ixp 8832

This theorem is referenced by:  fvixp  8836  ixpfn  8837  elixp  8838  ixpf  8854  resixp  8867  undifixp  8868  mptelixpg  8869  prdsbasprj  17394  xpsfrnel  17484  xpscf  17487  isssc  17745  isfuncd  17790  funcres2b  17822  dprdw  19909  ptrecube  37602  kelac1  43039  elixpconstg  45070  fvixp2  45180  rrxsnicc  46285  ioorrnopnxrlem  46291  hoiqssbllem1  46607  iinhoiicclem  46658  iunhoiioolem  46660  funcf2lem  49070  isnatd  49212